Theorem f1oeq1 6763

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 6726	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6743	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6500	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6500	. 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 1542  –1-1→wf1 6490  –onto→wfo 6491  –1-1-onto→wf1o 6492

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500

This theorem is referenced by:  f1oeq123d  6769  f1oeq1d  6770  f1ocnvb  6788  resin  6797  f1ovi  6815  f1oresrab  7075  fsn  7083  f1ounsn  7221  fveqf1o  7251  isoeq1  7266  f1oexbi  7873  oacomf1o  8494  mapsnd  8828  mapsnf1o3  8837  f1oen4g  8905  f1oen3g  8907  en0  8959  en0r  8961  ensn1  8962  en2sn  8982  en2prd  8988  xpcomf1o  8998  omf1o  9012  enfixsn  9018  domss2  9068  ssfiALT  9102  php3  9137  isinf  9169  oef1o  9613  cnfcom  9615  cnfcom3  9619  infxpenc  9934  ackbij2lem2  10155  ackbij2  10158  canthp1lem2  10570  pwfseqlem5  10580  seqf1olem2  13998  seqf1o  13999  hasheqf1oi  14307  hashf1rn  14308  hasheqf1od  14309  hashfacen  14410  wrd2f1tovbij  14916  s7f1o  14922  summo  15673  fsum  15676  ackbijnn  15787  prodmo  15895  fprod  15900  sadcaddlem  16420  unbenlem  16873  setcinv  18051  equivestrcsetc  18112  isgim  19231  symgval  19340  elsymgbas2  19342  symg1bas  19360  cayleyth  19384  gsumval3eu  19873  gsumval3lem1  19874  gsumval3lem2  19875  islmim  21052  uvcendim  21840  coe1mul2lem2  22246  mdet0f1o  22571  resinf1o  26516  efif1olem4  26525  logf1o  26544  relogf1o  26546  dvlog  26631  2lgslem1  27374  isismt  28619  nbusgrf1o1  29456  cusgrfilem3  29544  wwlksnextbij  29988  wlksnwwlknvbij  29994  clwwlkvbij  30201  hoif  31843  rabfodom  32593  fresf1o  32722  fpwrelmapffs  32825  fzo0pmtrlast  33171  pmtridf1o  33173  cycpmconjslem2  33234  1arithidomlem1  33613  1arithidom  33615  eulerpartlem1  34530  eulerpartgbij  34535  eulerpart  34545  derangenlem  35372  subfacp1lem2a  35381  subfacp1lem3  35383  subfacp1lem5  35385  subfacp1lem6  35386  subfacp1  35387  f1omptsn  37670  poimirlem3  37961  poimirlem4  37962  poimirlem5  37963  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem9  37967  poimirlem10  37968  poimirlem11  37969  poimirlem12  37970  poimirlem13  37971  poimirlem14  37972  poimirlem15  37973  poimirlem16  37974  poimirlem17  37975  poimirlem18  37976  poimirlem19  37977  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem25  37983  poimirlem26  37984  poimirlem27  37985  poimirlem29  37987  poimirlem31  37989  isismty  38139  isrngoiso  38316  islaut  40546  ispautN  40562  aks6d1c2  42586  sticksstones4  42605  sticksstones20  42622  eldioph2lem1  43209  pwfi2f1o  43545  rfovcnvf1od  44452  clsneif1o  44552  neicvgf1o  44562  nregmodelf1o  45463  3f1oss1  47538  fundcmpsurbijinjpreimafv  47882  sprbisymrel  47974  prproropen  47983  grimidvtxedg  48376  grimcnv  48379  grimco  48380  isuspgrim0  48385  gricushgr  48408  ushggricedg  48418  uhgrimisgrgric  48422  isgrtri  48434  isubgr3stgrlem3  48459  isubgr3stgr  48466  isgrlim  48473  uspgrlim  48483  grlicref  48503  grlicsym  48504  grlictr  48506  uspgrbispr  48642  uspgrbisymrelALT  48646  1aryenef  49136  2aryenef  49147  rrx2xpreen  49210  thincciso  49943  thinccisod  49944