Theorem f1oeq3 5809

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 5778	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5793	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 710	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5595	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5595	. 2 |- ( F : C -1-1-onto-> B <-> ( F : C -1-1-> B /\ F : C -onto-> B ) )
6	3, 4, 5	3bitr4g 288	1 |- ( A = B -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   -1-1->wf1 5585   -onto->wfo 5586   -1-1-onto->wf1o 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595

This theorem is referenced by:  f1oeq23  5810  f1oeq123d  5813  f1ores  5830  resdif  5836  resin  5837  f1osng  5854  f1oresrab  6054  fveqf1o  6194  isoeq5  6208  isoini2  6224  ncanth  6244  oacomf1o  7215  mapsnf1o  7511  bren  7526  xpcomf1o  7607  domss2  7677  isinf  7734  wemapwe  8140  wemapweOLD  8141  oef1o  8142  oef1oOLD  8143  cnfcomlem  8144  cnfcom2  8147  cnfcom3  8149  cnfcom3clem  8150  cnfcomlemOLD  8152  cnfcom2OLD  8155  cnfcom3OLD  8157  cnfcom3clemOLD  8158  infxpenc  8396  infxpenc2lem1  8397  infxpenc2  8400  infxpencOLD  8401  infxpenc2OLD  8404  ackbij2lem2  8621  fin1a2lem6  8786  hsmexlem1  8807  pwfseqlem5  9042  pwfseq  9043  hashgf1o  12050  axdc4uzlem  12061  sumeq1  13477  fsumss  13513  fsumcnv  13554  unbenlem  14288  4sqlem11  14335  pwssnf1o  14756  catcisolem  15294  yoniso  15415  xpsmnd  15782  gsumvalx  15827  gsumpropd  15829  gsumpropd2lem  15830  xpsgrp  16003  cayley  16253  cayleyth  16254  gsumval3OLD  16723  gsumval3lem1  16724  gsumval3lem2  16725  gsumcom2  16818  coe1mul2lem2  18120  scmatrngiso  18845  m2cpmrngiso  19066  cncfcnvcn  21252  ovolicc2lem4  21758  logf1o2  22856  uslgraf1oedg  24132  clwwlkvbij  24574  iseupa  24738  adjbd1o  26777  rinvf1o  27242  eulerpartgbij  28062  eulerpartlemgh  28068  derangval  28362  subfacp1lem2a  28375  subfacp1lem3  28377  subfacp1lem5  28379  mrsubff1o  28626  msubff1o  28668  elgiso  28787  prodeq1f  28893  fprodss  28933  fprodcnv  28966  ismtyval  30126  ismrer1  30164  rngoisoval  30210  pwfi2f1o  30875  imasgim  30879  bj-finsumval0  33952  lautset  35095  pautsetN  35111  hvmap1o2  36779