Theorem f1oeq1 6779

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 6740	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6759	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 640	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6513	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6513	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1550  –1-1→wf1 6503  –onto→wfo 6504  –1-1-onto→wf1o 6505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513

This theorem is referenced by:  f1oeq123d  6785  f1oeq1d  6786  f1ocnvb  6805  resin  6814  f1ovi  6832  f1oresrab  7094  fsn  7102  f1ounsn  7241  fveqf1o  7271  isoeq1  7286  f1oexbi  7894  oacomf1o  8518  mapsnd  8853  mapsnf1o3  8862  f1oen4g  8930  f1oen3g  8932  en0  8984  en0r  8986  ensn1  8987  en2sn  9007  en2prd  9013  xpcomf1o  9023  omf1o  9037  enfixsn  9043  domss2  9093  ssfiALT  9127  php3  9162  isinf  9194  oef1o  9639  cnfcom  9641  cnfcom3  9645  infxpenc  9960  ackbij2lem2  10181  ackbij2  10184  canthp1lem2  10597  pwfseqlem5  10607  seqf1olem2  14041  seqf1o  14042  hasheqf1oi  14350  hashf1rn  14351  hasheqf1od  14352  hashfacen  14453  wrd2f1tovbij  14959  s7f1o  14965  summo  15716  fsum  15719  ackbijnn  15830  prodmo  15938  fprod  15943  sadcaddlem  16463  unbenlem  16916  setcinv  18095  equivestrcsetc  18156  isgim  19274  symgval  19383  elsymgbas2  19385  symg1bas  19403  cayleyth  19427  gsumval3eu  19916  gsumval3lem1  19917  gsumval3lem2  19918  islmim  21098  uvcendim  21868  coe1mul2lem2  22300  mdet0f1o  22622  resinf1o  26567  efif1olem4  26576  logf1o  26595  relogf1o  26597  dvlog  26682  2lgslem1  27424  isismt  28669  nbusgrf1o1  29506  cusgrfilem3  29593  wwlksnextbij  30037  wlksnwwlknvbij  30043  clwwlkvbij  30250  hoif  31892  rabfodom  32642  fresf1o  32772  fpwrelmapffs  32875  fzo0pmtrlast  33222  pmtridf1o  33224  cycpmconjslem2  33285  1arithidomlem1  33675  1arithidom  33677  eulerpartlem1  34608  eulerpartgbij  34613  eulerpart  34623  derangenlem  35459  subfacp1lem2a  35468  subfacp1lem3  35470  subfacp1lem5  35472  subfacp1lem6  35473  subfacp1  35474  f1omptsn  37769  poimirlem3  38060  poimirlem4  38061  poimirlem5  38062  poimirlem6  38063  poimirlem7  38064  poimirlem8  38065  poimirlem9  38066  poimirlem10  38067  poimirlem11  38068  poimirlem12  38069  poimirlem13  38070  poimirlem14  38071  poimirlem15  38072  poimirlem16  38073  poimirlem17  38074  poimirlem18  38075  poimirlem19  38076  poimirlem20  38077  poimirlem21  38078  poimirlem22  38079  poimirlem25  38082  poimirlem26  38083  poimirlem27  38084  poimirlem29  38086  poimirlem31  38088  isismty  38238  isrngoiso  38415  islaut  40645  ispautN  40661  aks6d1c2  42685  sticksstones4  42704  sticksstones20  42721  eldioph2lem1  43279  pwfi2f1o  43611  rfovcnvf1od  44518  clsneif1o  44618  neicvgf1o  44628  nregmodelf1o  45529  3f1oss1  47607  fundcmpsurbijinjpreimafv  47951  sprbisymrel  48043  prproropen  48052  grimidvtxedg  48445  grimcnv  48448  grimco  48449  isuspgrim0  48454  gricushgr  48477  ushggricedg  48487  uhgrimisgrgric  48491  isgrtri  48503  isubgr3stgrlem3  48528  isubgr3stgr  48535  isgrlim  48542  uspgrlim  48552  grlicref  48572  grlicsym  48573  grlictr  48575  uspgrbispr  48711  uspgrbisymrelALT  48715  1aryenef  49205  2aryenef  49216  rrx2xpreen  49279  thincciso  50012  thinccisod  50013