Theorem f1oeq1 6817

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 6778	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6797	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6550	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6550	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  –1-1→wf1 6540  –onto→wfo 6541  –1-1-onto→wf1o 6542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is used by:  f1oeq123d  6823  f1oeq1d  6824  f1ocnvb  6843  resin  6852  f1ovi  6870  f1oresrab  7133  fsn  7141  f1ounsn  7284  fveqf1o  7314  isoeq1  7329  f1oexbi  7944  oacomf1o  8580  mapsnd  8921  mapsnf1o3  8930  f1oen4g  8998  f1oen3g  9000  en0  9052  en0r  9054  ensn1  9055  en2sn  9076  en2prd  9082  xpcomf1o  9092  omf1o  9106  enfixsn  9112  domss2  9162  ssfiALT  9196  php3  9231  isinf  9263  oef1o  9706  cnfcom  9708  cnfcom3  9712  infxpenc  10104  ackbij2lem2  10324  ackbij2  10327  canthp1lem2  10745  pwfseqlem5  10755  seqf1olem2  14192  seqf1o  14193  hasheqf1oi  14502  hashf1rn  14503  hasheqf1od  14504  hashfacen  14606  wrd2f1tovbij  15122  s7f1o  15128  summo  15892  fsum  15895  ackbijnn  16006  prodmo  16112  fprod  16117  sadcaddlem  16636  unbenlem  17095  setcinv  18274  equivestrcsetc  18335  isgim  19485  symgval  19594  elsymgbas2  19596  symg1bas  19614  cayleyth  19638  gsumval3eu  20127  gsumval3lem1  20128  gsumval3lem2  20129  rimval  20739  islmim  21346  uvcendim  22162  coe1mul2lem2  22596  mdet0f1o  22917  resinf1o  26873  efif1olem4  26882  logf1o  26901  relogf1o  26903  dvlog  26988  2lgslem1  27730  isismt  29006  nbusgrf1o1  29960  cusgrfilem3  30047  wwlksnextbij  30500  wlksnwwlknvbij  30506  clwwlkvbij  30713  hoif  32365  rabfodom  33152  fresf1o  33276  fpwrelmapffs  33376  fzo0pmtrlast  33703  pmtridf1o  33705  cycpmconjslem2  33766  1arithidomlem1  34117  1arithidom  34119  eulerpartlem1  35049  eulerpartgbij  35054  eulerpart  35064  derangenlem  36026  subfacp1lem2a  36035  subfacp1lem3  36037  subfacp1lem5  36039  subfacp1lem6  36040  subfacp1  36041  f1omptsn  38369  poimirlem3  38650  poimirlem4  38651  poimirlem5  38652  poimirlem6  38653  poimirlem7  38654  poimirlem8  38655  poimirlem9  38656  poimirlem10  38657  poimirlem11  38658  poimirlem12  38659  poimirlem13  38660  poimirlem14  38661  poimirlem15  38662  poimirlem16  38663  poimirlem17  38664  poimirlem18  38665  poimirlem19  38666  poimirlem20  38667  poimirlem21  38668  poimirlem22  38669  poimirlem25  38672  poimirlem26  38673  poimirlem27  38674  poimirlem29  38676  poimirlem31  38678  isismty  38844  isrngoiso  39021  islaut  41249  ispautN  41265  aks6d1c2  43289  sticksstones4  43308  sticksstones20  43325  eldioph2lem1  43880  pwfi2f1o  44207  rfovcnvf1od  45113  clsneif1o  45213  neicvgf1o  45223  nregmodelf1o  46113  3f1oss1  48253  fundcmpsurbijinjpreimafv  48597  sprbisymrel  48689  prproropen  48698  grimidvtxedg  49091  grimcnv  49094  grimco  49095  isuspgrim0  49100  gricushgr  49123  ushggricedg  49133  uhgrimisgrgric  49137  isgrtri  49149  isubgr3stgrlem3  49174  isubgr3stgr  49181  isgrlim  49188  uspgrlim  49198  grlicref  49218  grlicsym  49219  grlictr  49221  uspgrbispr  49357  uspgrbisymrelALT  49361  1aryenef  49865  2aryenef  49876  rrx2xpreen  49940  thincciso  50696  thinccisod  50697