Theorem f1oeq3 5791

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 5760	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5775	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 708	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5577	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5577	. 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 367   = wceq 1398   -1-1->wf1 5567   -onto->wfo 5568   -1-1-onto->wf1o 5569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577

This theorem is referenced by:  f1oeq23  5792  f1oeq123d  5795  f1ores  5812  resdif  5818  resin  5819  f1osng  5836  f1oresrab  6039  fveqf1o  6180  isoeq5  6194  isoini2  6210  ncanth  6230  oacomf1o  7206  mapsnf1o  7503  bren  7518  xpcomf1o  7599  domss2  7669  isinf  7726  wemapwe  8130  wemapweOLD  8131  oef1o  8132  oef1oOLD  8133  cnfcomlem  8134  cnfcom2  8137  cnfcom3  8139  cnfcom3clem  8140  cnfcomlemOLD  8142  cnfcom2OLD  8145  cnfcom3OLD  8147  cnfcom3clemOLD  8148  infxpenc  8386  infxpenc2lem1  8387  infxpenc2  8390  infxpencOLD  8391  infxpenc2OLD  8394  ackbij2lem2  8611  fin1a2lem6  8776  hsmexlem1  8797  pwfseqlem5  9030  pwfseq  9031  hashgf1o  12063  axdc4uzlem  12074  sumeq1  13593  fsumss  13629  fsumcnv  13670  prodeq1f  13797  fprodss  13837  fprodcnv  13869  unbenlem  14510  4sqlem11  14557  pwssnf1o  14987  catcisolem  15584  equivestrcsetc  15620  yoniso  15753  gsumvalx  16096  gsumpropd  16098  gsumpropd2lem  16099  xpsmnd  16159  xpsgrp  16388  cayley  16638  cayleyth  16639  gsumval3OLD  17107  gsumval3lem1  17108  gsumval3lem2  17109  gsumcom2  17199  coe1mul2lem2  18504  scmatrngiso  19205  m2cpmrngiso  19426  cncfcnvcn  21591  ovolicc2lem4  22097  logf1o2  23199  uslgraf1oedg  24561  clwwlkvbij  25003  iseupa  25167  adjbd1o  27202  rinvf1o  27691  eulerpartgbij  28575  eulerpartlemgh  28581  derangval  28875  subfacp1lem2a  28888  subfacp1lem3  28890  subfacp1lem5  28892  mrsubff1o  29139  msubff1o  29181  elgiso  29300  ismtyval  30536  ismrer1  30574  rngoisoval  30620  pwfi2f1o  31283  pwfi2f1oOLD  31284  imasgim  31289  bj-finsumval0  35063  lautset  36203  pautsetN  36219  hvmap1o2  37889