Theorem f1oeq1 6127

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

Assertion

Ref	Expression
f1oeq1	|- ( F = G -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )

Proof of Theorem f1oeq1

Step	Hyp	Ref	Expression
1		f1eq1 6096	. . 3 |- ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )
2		foeq1 6111	. . 3 |- ( F = G -> ( F : A -onto-> B <-> G : A -onto-> B ) )
3	1, 2	anbi12d 747	. 2 |- ( F = G -> ( ( F : A -1-1-> B /\ F : A -onto-> B ) <-> ( G : A -1-1-> B /\ G : A -onto-> B ) ) )
4		df-f1o 5895	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
5		df-f1o 5895	. 2 |- ( G : A -1-1-onto-> B <-> ( G : A -1-1-> B /\ G : A -onto-> B ) )
6	3, 4, 5	3bitr4g 303	1 |- ( F = G -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )

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-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1oeq123d  6133  f1ocnvb  6150  f1orescnv  6152  resin  6158  f1ovi  6175  f1osng  6177  f1oresrab  6395  fsn  6402  fveqf1o  6557  isoeq1  6567  f1oexbi  7116  oacomf1o  7645  mapsn  7899  mapsnf1o3  7906  f1oen3g  7971  ensn1  8020  xpcomf1o  8049  omf1o  8063  enfixsn  8069  domss2  8119  php3  8146  isinf  8173  ssfi  8180  oef1o  8595  cnfcomlem  8596  cnfcom  8597  cnfcom2  8599  cnfcom3  8601  cnfcom3clem  8602  infxpenc  8841  infxpenc2lem2  8843  infxpenc2  8845  ackbij2lem2  9062  ackbij2  9065  canthp1lem2  9475  pwfseqlem5  9485  pwfseq  9486  seqf1olem2  12841  seqf1o  12842  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashf1rn  13142  hashf1rnOLD  13143  hasheqf1od  13144  hashfacen  13238  wrd2f1tovbij  13703  summo  14448  fsum  14451  ackbijnn  14560  prodmo  14666  fprod  14671  bitsf1ocnv  15166  sadcaddlem  15179  unbenlem  15612  setcinv  16740  equivestrcsetc  16792  yonffthlem  16922  grplactcnv  17518  eqgen  17647  isgim  17704  elsymgbas2  17801  symg1bas  17816  cayleyth  17835  gsumval3eu  18305  gsumval3lem1  18306  gsumval3lem2  18307  islmim  19062  coe1mul2lem2  19638  znunithash  19913  uvcendim  20186  mdet0f1o  20399  tgpconncompeqg  21915  resinf1o  24282  efif1olem4  24291  logf1o  24311  relogf1o  24313  dvlog  24397  2lgslem1  25119  isismt  25429  nbusgrf1o1  26272  cusgrfilem3  26353  wlkisowwlkupgr  26766  wlknwwlksnbij2  26778  wlkwwlkbij2  26785  wwlksnextbij  26797  wlksnwwlknvbij  26803  clwwlksbij  26920  clwwlksvbij  26922  numclwlk1lem2  27230  hoif  28613  rabfodom  29344  fresf1o  29433  fcobijfs  29501  fpwrelmapffs  29509  gsummpt2d  29781  pmtridf1o  29856  indf1o  30086  eulerpartlem1  30429  eulerpartgbij  30434  eulerpart  30444  derangenlem  31153  subfacp1lem2a  31162  subfacp1lem3  31164  subfacp1lem5  31166  subfacp1lem6  31167  subfacp1  31168  f1omptsn  33184  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  isismty  33600  ismrer1  33637  isrngoiso  33777  islaut  35369  ispautN  35385  hvmap1o  37052  eldioph2lem1  37323  pwfi2f1o  37666  rfovcnvf1od  38298  clsneif1o  38402  neicvgf1o  38412  f1oeq1d  39363  mapsnd  39388  sprbisymrel  41749  uspgrbispr  41759  uspgrbisymrelALT  41763