Theorem f1oeq1 6688

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 6649	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6668	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6425	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6425	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  –1-1→wf1 6415  –onto→wfo 6416  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1oeq123d  6694  f1oeq1d  6695  f1ocnvb  6713  resin  6721  f1ovi  6738  f1oresrab  6981  fsn  6989  fveqf1o  7155  isoeq1  7168  f1oexbi  7749  oacomf1o  8358  mapsnd  8632  mapsnf1o3  8641  f1oen3g  8709  en0  8758  en0OLD  8759  ensn1  8761  ensn1OLD  8762  en2sn  8785  en2snOLD  8786  xpcomf1o  8801  omf1o  8815  enfixsn  8821  domss2  8872  php3  8899  ssfiALT  8919  isinf  8965  oef1o  9386  cnfcom  9388  cnfcom3  9392  infxpenc  9705  ackbij2lem2  9927  ackbij2  9930  canthp1lem2  10340  pwfseqlem5  10350  seqf1olem2  13691  seqf1o  13692  hasheqf1oi  13994  hashf1rn  13995  hasheqf1od  13996  hashfacen  14094  hashfacenOLD  14095  wrd2f1tovbij  14603  summo  15357  fsum  15360  ackbijnn  15468  prodmo  15574  fprod  15579  sadcaddlem  16092  unbenlem  16537  setcinv  17721  equivestrcsetc  17785  isgim  18793  symgval  18891  elsymgbas2  18895  symg1bas  18913  cayleyth  18938  gsumval3eu  19420  gsumval3lem1  19421  gsumval3lem2  19422  islmim  20239  uvcendim  20964  coe1mul2lem2  21349  mdet0f1o  21650  resinf1o  25597  efif1olem4  25606  logf1o  25625  relogf1o  25627  dvlog  25711  2lgslem1  26447  isismt  26799  nbusgrf1o1  27640  cusgrfilem3  27727  wwlksnextbij  28168  wlksnwwlknvbij  28174  clwwlkvbij  28378  hoif  30017  rabfodom  30752  fresf1o  30867  fpwrelmapffs  30971  pmtridf1o  31263  cycpmconjslem2  31324  eulerpartlem1  32234  eulerpartgbij  32239  eulerpart  32249  derangenlem  33033  subfacp1lem2a  33042  subfacp1lem3  33044  subfacp1lem5  33046  subfacp1lem6  33047  subfacp1  33048  f1omptsn  35435  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  isismty  35886  isrngoiso  36063  islaut  38024  ispautN  38040  sticksstones4  40033  sticksstones20  40050  eldioph2lem1  40498  pwfi2f1o  40837  rfovcnvf1od  41501  clsneif1o  41603  neicvgf1o  41613  fundcmpsurbijinjpreimafv  44747  sprbisymrel  44839  prproropen  44848  isomgreqve  45165  isomushgr  45166  isomuspgrlem2  45173  isomgrsym  45176  isomgrtr  45179  ushrisomgr  45181  uspgrbispr  45201  uspgrbisymrelALT  45205  1aryenef  45879  2aryenef  45890  rrx2xpreen  45953  thincciso  46218