Theorem f1oeq1 6777

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 6738	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6757	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6508	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6508	. 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 396   = wceq 1541  –1-1→wf1 6498  –onto→wfo 6499  –1-1-onto→wf1o 6500

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508

This theorem is referenced by:  f1oeq123d  6783  f1oeq1d  6784  f1ocnvb  6802  resin  6811  f1ovi  6828  f1oresrab  7078  fsn  7086  fveqf1o  7254  isoeq1  7267  f1oexbi  7870  oacomf1o  8517  mapsnd  8831  mapsnf1o3  8840  f1oen4g  8911  f1oen3g  8913  en0  8964  en0OLD  8965  en0r  8967  ensn1  8968  ensn1OLD  8969  en2sn  8992  en2snOLD  8993  en2prd  8999  xpcomf1o  9012  omf1o  9026  enfixsn  9032  domss2  9087  ssfiALT  9125  php3  9163  php3OLD  9175  isinf  9211  isinfOLD  9212  oef1o  9643  cnfcom  9645  cnfcom3  9649  infxpenc  9963  ackbij2lem2  10185  ackbij2  10188  canthp1lem2  10598  pwfseqlem5  10608  seqf1olem2  13958  seqf1o  13959  hasheqf1oi  14261  hashf1rn  14262  hasheqf1od  14263  hashfacen  14363  hashfacenOLD  14364  wrd2f1tovbij  14861  summo  15613  fsum  15616  ackbijnn  15724  prodmo  15830  fprod  15835  sadcaddlem  16348  unbenlem  16791  setcinv  17990  equivestrcsetc  18054  isgim  19066  symgval  19164  elsymgbas2  19168  symg1bas  19186  cayleyth  19211  gsumval3eu  19695  gsumval3lem1  19696  gsumval3lem2  19697  islmim  20580  uvcendim  21290  coe1mul2lem2  21676  mdet0f1o  21979  resinf1o  25929  efif1olem4  25938  logf1o  25957  relogf1o  25959  dvlog  26043  2lgslem1  26779  isismt  27539  nbusgrf1o1  28381  cusgrfilem3  28468  wwlksnextbij  28910  wlksnwwlknvbij  28916  clwwlkvbij  29120  hoif  30759  rabfodom  31496  fresf1o  31612  fpwrelmapffs  31719  pmtridf1o  32013  cycpmconjslem2  32074  eulerpartlem1  33056  eulerpartgbij  33061  eulerpart  33071  derangenlem  33852  subfacp1lem2a  33861  subfacp1lem3  33863  subfacp1lem5  33865  subfacp1lem6  33866  subfacp1  33867  f1omptsn  35881  poimirlem3  36154  poimirlem4  36155  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem9  36160  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem13  36164  poimirlem14  36165  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem18  36169  poimirlem19  36170  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  poimirlem29  36180  poimirlem31  36182  isismty  36333  isrngoiso  36510  islaut  38619  ispautN  38635  sticksstones4  40630  sticksstones20  40647  eldioph2lem1  41141  pwfi2f1o  41481  rfovcnvf1od  42398  clsneif1o  42498  neicvgf1o  42508  fundcmpsurbijinjpreimafv  45719  sprbisymrel  45811  prproropen  45820  isomgreqve  46137  isomushgr  46138  isomuspgrlem2  46145  isomgrsym  46148  isomgrtr  46151  ushrisomgr  46153  uspgrbispr  46173  uspgrbisymrelALT  46177  1aryenef  46851  2aryenef  46862  rrx2xpreen  46925  thincciso  47189