Theorem f1oeq3 5820

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

Assertion

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

Proof of Theorem f1oeq3

Step	Hyp	Ref	Expression
1		f1eq3 5789	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5804	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 725	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5596	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5596	. 2 |- ( F : C -1-1-onto-> B <-> ( F : C -1-1-> B /\ F : C -onto-> B ) )
6	3, 4, 5	3bitr4g 296	1 |- ( A = B -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   -1-1->wf1 5586   -onto->wfo 5587   -1-1-onto->wf1o 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596

This theorem is referenced by:  f1oeq23  5821  f1oeq123d  5824  f1oeq3d  5825  f1ores  5842  resdif  5848  resin  5849  f1osng  5867  f1oresrab  6071  fveqf1o  6218  isoeq5  6232  isoini2  6248  ncanth  6268  oacomf1o  7284  mapsnf1o  7581  bren  7596  xpcomf1o  7679  domss2  7749  isinf  7803  wemapwe  8220  oef1o  8221  cnfcomlem  8222  cnfcom2  8225  cnfcom3  8227  cnfcom3clem  8228  infxpenc  8467  infxpenc2lem1  8468  infxpenc2  8471  ackbij2lem2  8688  fin1a2lem6  8853  hsmexlem1  8874  pwfseqlem5  9106  pwfseq  9107  hashgf1o  12222  axdc4uzlem  12233  sumeq1  13832  fsumss  13868  fsumcnv  13911  prodeq1f  14039  fprodss  14079  fprodcnv  14114  unbenlem  14931  4sqlem11  14978  pwssnf1o  15474  catcisolem  16079  equivestrcsetc  16115  yoniso  16248  gsumvalx  16591  gsumpropd  16593  gsumpropd2lem  16594  xpsmnd  16654  xpsgrp  16883  cayley  17133  cayleyth  17134  gsumval3lem1  17617  gsumval3lem2  17618  gsumcom2  17685  coe1mul2lem2  18938  scmatrngiso  19638  m2cpmrngiso  19859  cncfcnvcn  22031  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  logf1o2  23674  uslgraf1oedg  25165  clwwlkvbij  25608  iseupa  25772  adjbd1o  27819  rinvf1o  28306  eulerpartgbij  29278  eulerpartlemgh  29284  derangval  29962  subfacp1lem2a  29975  subfacp1lem3  29977  subfacp1lem5  29979  mrsubff1o  30225  msubff1o  30267  elgiso  30386  bj-finsumval0  31772  f1omptsnlem  31808  f1omptsn  31809  poimirlem4  32008  poimirlem9  32013  poimirlem15  32019  ismtyval  32196  ismrer1  32234  rngoisoval  32280  lautset  33718  pautsetN  33734  hvmap1o2  35404  pwfi2f1o  36025  imasgim  36029  uspgrf1oedg  39421  usgrf1oedg  39452