Theorem f1oeq1 6579

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

Assertion

Ref	Expression
f1oeq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Proof of Theorem f1oeq1

Step	Hyp	Ref	Expression
1		f1eq1 6544	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6561	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6331	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6331	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  –1-1→wf1 6321  –onto→wfo 6322  –1-1-onto→wf1o 6323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331

This theorem is referenced by:  f1oeq123d  6585  f1ocnvb  6603  f1orescnv  6605  resin  6611  f1ovi  6628  f1osng  6630  f1oresrab  6866  fsn  6874  fveqf1o  7037  isoeq1  7049  f1oexbi  7615  oacomf1o  8174  mapsnd  8433  mapsnf1o3  8442  f1oen3g  8508  ensn1  8556  xpcomf1o  8589  omf1o  8603  enfixsn  8609  domss2  8660  php3  8687  isinf  8715  ssfi  8722  oef1o  9145  cnfcomlem  9146  cnfcom  9147  cnfcom2  9149  cnfcom3  9151  cnfcom3clem  9152  infxpenc  9429  infxpenc2lem2  9431  infxpenc2  9433  ackbij2lem2  9651  ackbij2  9654  canthp1lem2  10064  pwfseqlem5  10074  pwfseq  10075  seqf1olem2  13406  seqf1o  13407  hasheqf1oi  13708  hashf1rn  13709  hasheqf1od  13710  hashfacen  13808  wrd2f1tovbij  14315  summo  15066  fsum  15069  ackbijnn  15175  prodmo  15282  fprod  15287  bitsf1ocnv  15783  sadcaddlem  15796  unbenlem  16234  setcinv  17342  equivestrcsetc  17394  yonffthlem  17524  grplactcnv  18194  eqgen  18325  isgim  18394  symgval  18489  elsymgbas2  18493  symg1bas  18511  cayleyth  18535  gsumval3eu  19017  gsumval3lem1  19018  gsumval3lem2  19019  islmim  19827  znunithash  20256  uvcendim  20536  coe1mul2lem2  20897  mdet0f1o  21198  tgpconncompeqg  22717  resinf1o  25128  efif1olem4  25137  logf1o  25156  relogf1o  25158  dvlog  25242  2lgslem1  25978  isismt  26328  nbusgrf1o1  27160  cusgrfilem3  27247  wwlksnextbij  27688  wlksnwwlknvbij  27694  clwwlkvbij  27898  hoif  29537  rabfodom  30274  fresf1o  30390  fcobijfs  30485  fpwrelmapffs  30496  s2f1  30647  gsummpt2d  30734  pmtridf1o  30786  cycpmconjslem2  30847  indf1o  31393  eulerpartlem1  31735  eulerpartgbij  31740  eulerpart  31750  derangenlem  32531  subfacp1lem2a  32540  subfacp1lem3  32542  subfacp1lem5  32544  subfacp1lem6  32545  subfacp1  32546  f1omptsn  34754  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem29  35086  poimirlem31  35088  isismty  35239  ismrer1  35276  isrngoiso  35416  islaut  37379  ispautN  37395  hvmap1o  39059  eldioph2lem1  39701  pwfi2f1o  40040  rfovcnvf1od  40705  clsneif1o  40807  neicvgf1o  40817  f1oeq1d  41805  fundcmpsurbijinjpreimafv  43924  sprbisymrel  44016  prproropen  44025  isomgreqve  44343  isomushgr  44344  isomuspgrlem2  44351  isomgrsym  44354  isomgrtr  44357  ushrisomgr  44359  uspgrbispr  44379  uspgrbisymrelALT  44383  1aryenef  45059  2aryenef  45070  rrx2xpreen  45133