Theorem f1oeq1 6822

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 6783	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6802	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6551	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6551	. 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 205   ∧ wa 397   = wceq 1542  –1-1→wf1 6541  –onto→wfo 6542  –1-1-onto→wf1o 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551

This theorem is referenced by:  f1oeq123d  6828  f1oeq1d  6829  f1ocnvb  6847  resin  6856  f1ovi  6873  f1oresrab  7125  fsn  7133  fveqf1o  7301  isoeq1  7314  f1oexbi  7919  oacomf1o  8565  mapsnd  8880  mapsnf1o3  8889  f1oen4g  8960  f1oen3g  8962  en0  9013  en0OLD  9014  en0r  9016  ensn1  9017  ensn1OLD  9018  en2sn  9041  en2snOLD  9042  en2prd  9048  xpcomf1o  9061  omf1o  9075  enfixsn  9081  domss2  9136  ssfiALT  9174  php3  9212  php3OLD  9224  isinf  9260  isinfOLD  9261  oef1o  9693  cnfcom  9695  cnfcom3  9699  infxpenc  10013  ackbij2lem2  10235  ackbij2  10238  canthp1lem2  10648  pwfseqlem5  10658  seqf1olem2  14008  seqf1o  14009  hasheqf1oi  14311  hashf1rn  14312  hasheqf1od  14313  hashfacen  14413  hashfacenOLD  14414  wrd2f1tovbij  14911  summo  15663  fsum  15666  ackbijnn  15774  prodmo  15880  fprod  15885  sadcaddlem  16398  unbenlem  16841  setcinv  18040  equivestrcsetc  18104  isgim  19136  symgval  19236  elsymgbas2  19240  symg1bas  19258  cayleyth  19283  gsumval3eu  19772  gsumval3lem1  19773  gsumval3lem2  19774  islmim  20673  uvcendim  21402  coe1mul2lem2  21790  mdet0f1o  22095  resinf1o  26045  efif1olem4  26054  logf1o  26073  relogf1o  26075  dvlog  26159  2lgslem1  26897  isismt  27785  nbusgrf1o1  28627  cusgrfilem3  28714  wwlksnextbij  29156  wlksnwwlknvbij  29162  clwwlkvbij  29366  hoif  31007  rabfodom  31743  fresf1o  31855  fpwrelmapffs  31959  pmtridf1o  32253  cycpmconjslem2  32314  eulerpartlem1  33366  eulerpartgbij  33371  eulerpart  33381  derangenlem  34162  subfacp1lem2a  34171  subfacp1lem3  34173  subfacp1lem5  34175  subfacp1lem6  34176  subfacp1  34177  f1omptsn  36218  poimirlem3  36491  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem29  36517  poimirlem31  36519  isismty  36669  isrngoiso  36846  islaut  38954  ispautN  38970  sticksstones4  40965  sticksstones20  40982  eldioph2lem1  41498  pwfi2f1o  41838  rfovcnvf1od  42755  clsneif1o  42855  neicvgf1o  42865  fundcmpsurbijinjpreimafv  46075  sprbisymrel  46167  prproropen  46176  isomgreqve  46493  isomushgr  46494  isomuspgrlem2  46501  isomgrsym  46504  isomgrtr  46507  ushrisomgr  46509  uspgrbispr  46529  uspgrbisymrelALT  46533  1aryenef  47331  2aryenef  47342  rrx2xpreen  47405  thincciso  47669