Theorem f1oeq3 5807

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 5776	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5791	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 717	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5589	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5589	. 2 |- ( F : C -1-1-onto-> B <-> ( F : C -1-1-> B /\ F : C -onto-> B ) )
6	3, 4, 5	3bitr4g 292	1 |- ( A = B -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   -1-1->wf1 5579   -onto->wfo 5580   -1-1-onto->wf1o 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589

This theorem is referenced by:  f1oeq23  5808  f1oeq123d  5811  f1ores  5828  resdif  5834  resin  5835  f1osng  5853  f1oresrab  6055  fveqf1o  6200  isoeq5  6214  isoini2  6230  ncanth  6250  oacomf1o  7266  mapsnf1o  7563  bren  7578  xpcomf1o  7661  domss2  7731  isinf  7785  wemapwe  8202  oef1o  8203  cnfcomlem  8204  cnfcom2  8207  cnfcom3  8209  cnfcom3clem  8210  infxpenc  8449  infxpenc2lem1  8450  infxpenc2  8453  ackbij2lem2  8670  fin1a2lem6  8835  hsmexlem1  8856  pwfseqlem5  9088  pwfseq  9089  hashgf1o  12184  axdc4uzlem  12195  sumeq1  13755  fsumss  13791  fsumcnv  13834  prodeq1f  13962  fprodss  14002  fprodcnv  14037  unbenlem  14852  4sqlem11  14899  pwssnf1o  15396  catcisolem  16001  equivestrcsetc  16037  yoniso  16170  gsumvalx  16513  gsumpropd  16515  gsumpropd2lem  16516  xpsmnd  16576  xpsgrp  16805  cayley  17055  cayleyth  17056  gsumval3lem1  17539  gsumval3lem2  17540  gsumcom2  17607  coe1mul2lem2  18861  scmatrngiso  19561  m2cpmrngiso  19782  cncfcnvcn  21953  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  logf1o2  23595  uslgraf1oedg  25086  clwwlkvbij  25529  iseupa  25693  adjbd1o  27738  rinvf1o  28230  eulerpartgbij  29205  eulerpartlemgh  29211  derangval  29890  subfacp1lem2a  29903  subfacp1lem3  29905  subfacp1lem5  29907  mrsubff1o  30153  msubff1o  30195  elgiso  30314  bj-finsumval0  31702  f1omptsnlem  31738  f1omptsn  31739  poimirlem4  31944  poimirlem9  31949  poimirlem15  31955  ismtyval  32132  ismrer1  32170  rngoisoval  32216  lautset  33647  pautsetN  33663  hvmap1o2  35333  pwfi2f1o  35954  imasgim  35958  f1oeq3d  37442  uspgrf1oedg  39260  usgrf1oedg  39290