Theorem f1oeq1 6770

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 6733	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6750	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6506	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6506	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  –1-1→wf1 6496  –onto→wfo 6497  –1-1-onto→wf1o 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1oeq123d  6776  f1oeq1d  6777  f1ocnvb  6795  resin  6804  f1ovi  6821  f1oresrab  7081  fsn  7089  f1ounsn  7229  fveqf1o  7259  isoeq1  7274  f1oexbi  7884  oacomf1o  8506  mapsnd  8836  mapsnf1o3  8845  f1oen4g  8913  f1oen3g  8915  en0  8966  en0r  8968  ensn1  8969  en2sn  8989  en2prd  8996  xpcomf1o  9007  omf1o  9021  enfixsn  9027  domss2  9077  ssfiALT  9115  php3  9150  isinf  9183  isinfOLD  9184  oef1o  9627  cnfcom  9629  cnfcom3  9633  infxpenc  9947  ackbij2lem2  10168  ackbij2  10171  canthp1lem2  10582  pwfseqlem5  10592  seqf1olem2  13983  seqf1o  13984  hasheqf1oi  14292  hashf1rn  14293  hasheqf1od  14294  hashfacen  14395  wrd2f1tovbij  14902  s7f1o  14908  summo  15659  fsum  15662  ackbijnn  15770  prodmo  15878  fprod  15883  sadcaddlem  16403  unbenlem  16855  setcinv  18032  equivestrcsetc  18093  isgim  19176  symgval  19285  elsymgbas2  19287  symg1bas  19305  cayleyth  19329  gsumval3eu  19818  gsumval3lem1  19819  gsumval3lem2  19820  islmim  21001  uvcendim  21789  coe1mul2lem2  22187  mdet0f1o  22513  resinf1o  26478  efif1olem4  26487  logf1o  26506  relogf1o  26508  dvlog  26593  2lgslem1  27338  isismt  28514  nbusgrf1o1  29350  cusgrfilem3  29438  wwlksnextbij  29882  wlksnwwlknvbij  29888  clwwlkvbij  30092  hoif  31733  rabfodom  32484  fresf1o  32605  fpwrelmapffs  32707  fzo0pmtrlast  33064  pmtridf1o  33066  cycpmconjslem2  33127  1arithidomlem1  33499  1arithidom  33501  eulerpartlem1  34351  eulerpartgbij  34356  eulerpart  34366  derangenlem  35151  subfacp1lem2a  35160  subfacp1lem3  35162  subfacp1lem5  35164  subfacp1lem6  35165  subfacp1  35166  f1omptsn  37318  poimirlem3  37610  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem9  37616  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem29  37636  poimirlem31  37638  isismty  37788  isrngoiso  37965  islaut  40070  ispautN  40086  aks6d1c2  42111  sticksstones4  42130  sticksstones20  42147  eldioph2lem1  42741  pwfi2f1o  43078  rfovcnvf1od  43986  clsneif1o  44086  neicvgf1o  44096  nregmodelf1o  44998  3f1oss1  47069  fundcmpsurbijinjpreimafv  47401  sprbisymrel  47493  prproropen  47502  grimidvtxedg  47878  grimcnv  47881  grimco  47882  isuspgrim0  47887  gricushgr  47910  ushggricedg  47920  uhgrimisgrgric  47924  isgrtri  47935  isubgr3stgrlem3  47960  isubgr3stgr  47967  isgrlim  47974  uspgrlim  47984  grlicref  47997  grlicsym  47998  grlictr  48000  uspgrbispr  48132  uspgrbisymrelALT  48136  1aryenef  48627  2aryenef  48638  rrx2xpreen  48701  thincciso  49435  thinccisod  49436