Theorem f1oeq1 6762

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 6725	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6742	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6499	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6499	. 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 1541  –1-1→wf1 6489  –onto→wfo 6490  –1-1-onto→wf1o 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  f1oeq123d  6768  f1oeq1d  6769  f1ocnvb  6787  resin  6796  f1ovi  6814  f1oresrab  7072  fsn  7080  f1ounsn  7218  fveqf1o  7248  isoeq1  7263  f1oexbi  7870  oacomf1o  8492  mapsnd  8824  mapsnf1o3  8833  f1oen4g  8901  f1oen3g  8903  en0  8955  en0r  8957  ensn1  8958  en2sn  8978  en2prd  8984  xpcomf1o  8994  omf1o  9008  enfixsn  9014  domss2  9064  ssfiALT  9098  php3  9133  isinf  9165  oef1o  9607  cnfcom  9609  cnfcom3  9613  infxpenc  9928  ackbij2lem2  10149  ackbij2  10152  canthp1lem2  10564  pwfseqlem5  10574  seqf1olem2  13965  seqf1o  13966  hasheqf1oi  14274  hashf1rn  14275  hasheqf1od  14276  hashfacen  14377  wrd2f1tovbij  14883  s7f1o  14889  summo  15640  fsum  15643  ackbijnn  15751  prodmo  15859  fprod  15864  sadcaddlem  16384  unbenlem  16836  setcinv  18014  equivestrcsetc  18075  isgim  19191  symgval  19300  elsymgbas2  19302  symg1bas  19320  cayleyth  19344  gsumval3eu  19833  gsumval3lem1  19834  gsumval3lem2  19835  islmim  21014  uvcendim  21802  coe1mul2lem2  22210  mdet0f1o  22537  resinf1o  26501  efif1olem4  26510  logf1o  26529  relogf1o  26531  dvlog  26616  2lgslem1  27361  isismt  28606  nbusgrf1o1  29443  cusgrfilem3  29531  wwlksnextbij  29975  wlksnwwlknvbij  29981  clwwlkvbij  30188  hoif  31829  rabfodom  32580  fresf1o  32709  fpwrelmapffs  32813  fzo0pmtrlast  33174  pmtridf1o  33176  cycpmconjslem2  33237  1arithidomlem1  33616  1arithidom  33618  eulerpartlem1  34524  eulerpartgbij  34529  eulerpart  34539  derangenlem  35365  subfacp1lem2a  35374  subfacp1lem3  35376  subfacp1lem5  35378  subfacp1lem6  35379  subfacp1  35380  f1omptsn  37542  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  poimirlem31  37852  isismty  38002  isrngoiso  38179  islaut  40343  ispautN  40359  aks6d1c2  42384  sticksstones4  42403  sticksstones20  42420  eldioph2lem1  43002  pwfi2f1o  43338  rfovcnvf1od  44245  clsneif1o  44345  neicvgf1o  44355  nregmodelf1o  45256  3f1oss1  47321  fundcmpsurbijinjpreimafv  47653  sprbisymrel  47745  prproropen  47754  grimidvtxedg  48131  grimcnv  48134  grimco  48135  isuspgrim0  48140  gricushgr  48163  ushggricedg  48173  uhgrimisgrgric  48177  isgrtri  48189  isubgr3stgrlem3  48214  isubgr3stgr  48221  isgrlim  48228  uspgrlim  48238  grlicref  48258  grlicsym  48259  grlictr  48261  uspgrbispr  48397  uspgrbisymrelALT  48401  1aryenef  48891  2aryenef  48902  rrx2xpreen  48965  thincciso  49698  thinccisod  49699