Theorem f1oeq1 6810

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 6771	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6790	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6544	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6544	. 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 1570  –1-1→wf1 6534  –onto→wfo 6535  –1-1-onto→wf1o 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is used by:  f1oeq123d  6816  f1oeq1d  6817  f1ocnvb  6836  resin  6845  f1ovi  6863  f1oresrab  7126  fsn  7134  f1ounsn  7278  fveqf1o  7308  isoeq1  7323  f1oexbi  7938  oacomf1o  8566  mapsnd  8907  mapsnf1o3  8916  f1oen4g  8984  f1oen3g  8986  en0  9038  en0r  9040  ensn1  9041  en2sn  9062  en2prd  9068  xpcomf1o  9078  omf1o  9092  enfixsn  9098  domss2  9148  ssfiALT  9182  php3  9217  isinf  9249  oef1o  9692  cnfcom  9694  cnfcom3  9698  infxpenc  10090  ackbij2lem2  10310  ackbij2  10313  canthp1lem2  10731  pwfseqlem5  10741  seqf1olem2  14178  seqf1o  14179  hasheqf1oi  14488  hashf1rn  14489  hasheqf1od  14490  hashfacen  14592  wrd2f1tovbij  15106  s7f1o  15112  summo  15876  fsum  15879  ackbijnn  15990  prodmo  16096  fprod  16101  sadcaddlem  16620  unbenlem  17079  setcinv  18258  equivestrcsetc  18319  isgim  19469  symgval  19578  elsymgbas2  19580  symg1bas  19598  cayleyth  19622  gsumval3eu  20111  gsumval3lem1  20112  gsumval3lem2  20113  rimval  20723  islmim  21330  uvcendim  22146  coe1mul2lem2  22580  mdet0f1o  22901  resinf1o  26857  efif1olem4  26866  logf1o  26885  relogf1o  26887  dvlog  26972  2lgslem1  27714  isismt  28990  nbusgrf1o1  29944  cusgrfilem3  30031  wwlksnextbij  30484  wlksnwwlknvbij  30490  clwwlkvbij  30697  hoif  32349  rabfodom  33094  fresf1o  33218  fpwrelmapffs  33319  fzo0pmtrlast  33646  pmtridf1o  33648  cycpmconjslem2  33709  1arithidomlem1  34060  1arithidom  34062  eulerpartlem1  34992  eulerpartgbij  34997  eulerpart  35007  derangenlem  35915  subfacp1lem2a  35924  subfacp1lem3  35926  subfacp1lem5  35928  subfacp1lem6  35929  subfacp1  35930  f1omptsn  38240  poimirlem3  38521  poimirlem4  38522  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem9  38527  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem29  38547  poimirlem31  38549  isismty  38715  isrngoiso  38892  islaut  41120  ispautN  41136  aks6d1c2  43160  sticksstones4  43179  sticksstones20  43196  eldioph2lem1  43750  pwfi2f1o  44082  rfovcnvf1od  44989  clsneif1o  45089  neicvgf1o  45099  nregmodelf1o  45983  3f1oss1  48114  fundcmpsurbijinjpreimafv  48458  sprbisymrel  48550  prproropen  48559  grimidvtxedg  48952  grimcnv  48955  grimco  48956  isuspgrim0  48961  gricushgr  48984  ushggricedg  48994  uhgrimisgrgric  48998  isgrtri  49010  isubgr3stgrlem3  49035  isubgr3stgr  49042  isgrlim  49049  uspgrlim  49059  grlicref  49079  grlicsym  49080  grlictr  49082  uspgrbispr  49218  uspgrbisymrelALT  49222  1aryenef  49726  2aryenef  49737  rrx2xpreen  49800  thincciso  50530  thinccisod  50531