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  27816  nbusgrf1o1  28658  cusgrfilem3  28745  wwlksnextbij  29187  wlksnwwlknvbij  29193  clwwlkvbij  29397  hoif  31038  rabfodom  31774  fresf1o  31886  fpwrelmapffs  31990  pmtridf1o  32284  cycpmconjslem2  32345  eulerpartlem1  33397  eulerpartgbij  33402  eulerpart  33412  derangenlem  34193  subfacp1lem2a  34202  subfacp1lem3  34204  subfacp1lem5  34206  subfacp1lem6  34207  subfacp1  34208  f1omptsn  36266  poimirlem3  36539  poimirlem4  36540  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem8  36544  poimirlem9  36545  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem13  36549  poimirlem14  36550  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem29  36565  poimirlem31  36567  isismty  36717  isrngoiso  36894  islaut  39002  ispautN  39018  sticksstones4  41013  sticksstones20  41030  eldioph2lem1  41546  pwfi2f1o  41886  rfovcnvf1od  42803  clsneif1o  42903  neicvgf1o  42913  fundcmpsurbijinjpreimafv  46123  sprbisymrel  46215  prproropen  46224  isomgreqve  46541  isomushgr  46542  isomuspgrlem2  46549  isomgrsym  46552  isomgrtr  46555  ushrisomgr  46557  uspgrbispr  46577  uspgrbisymrelALT  46581  1aryenef  47379  2aryenef  47390  rrx2xpreen  47453  thincciso  47717