Theorem f1oeq2 6128

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

Assertion

Ref	Expression
f1oeq2	|- ( A = B -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )

Proof of Theorem f1oeq2

Step	Hyp	Ref	Expression
1		f1eq2 6097	. . 3 |- ( A = B -> ( F : A -1-1-> C <-> F : B -1-1-> C ) )
2		foeq2 6112	. . 3 |- ( A = B -> ( F : A -onto-> C <-> F : B -onto-> C ) )
3	1, 2	anbi12d 747	. 2 |- ( A = B -> ( ( F : A -1-1-> C /\ F : A -onto-> C ) <-> ( F : B -1-1-> C /\ F : B -onto-> C ) ) )
4		df-f1o 5895	. 2 |- ( F : A -1-1-onto-> C <-> ( F : A -1-1-> C /\ F : A -onto-> C ) )
5		df-f1o 5895	. 2 |- ( F : B -1-1-onto-> C <-> ( F : B -1-1-> C /\ F : B -onto-> C ) )
6	3, 4, 5	3bitr4g 303	1 |- ( A = B -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1oeq23  6130  f1oeq123d  6133  resin  6158  f1osng  6177  f1o2sn  6408  fveqf1o  6557  isoeq4  6570  oacomf1o  7645  bren  7964  f1dmvrnfibi  8250  marypha1lem  8339  oef1o  8595  cnfcomlem  8596  cnfcom  8597  cnfcom2  8599  infxpenc  8841  infxpenc2  8845  pwfseqlem5  9485  pwfseq  9486  summolem3  14445  summo  14448  fsum  14451  fsumf1o  14454  sumsnf  14473  sumsn  14475  prodmolem3  14663  prodmo  14666  fprod  14671  fprodf1o  14676  prodsn  14692  prodsnf  14694  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  gsumval3lem1  18306  gsumval3  18308  znhash  19907  znunithash  19913  imasf1oxms  22294  cncfcnvcn  22724  wlksnwwlknvbij  26803  clwwlksvbij  26922  eupthp1  27076  f1ocnt  29559  derangval  31149  subfacp1lem2a  31162  subfacp1lem3  31164  subfacp1lem5  31166  erdsze2lem1  31185  ismtyval  33599  rngoisoval  33776  lautset  35368  pautsetN  35384  eldioph2lem1  37323  imasgim  37670  sumsnd  39185  f1oeq2d  39361  stoweidlem35  40252  stoweidlem39  40256  uspgrsprfo  41756