Theorem f1oeq1 6794

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 6755	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6774	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 641	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6528	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6528	. 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 399   = wceq 1560  –1-1→wf1 6518  –onto→wfo 6519  –1-1-onto→wf1o 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528

This theorem is referenced by:  f1oeq123d  6800  f1oeq1d  6801  f1ocnvb  6820  resin  6829  f1ovi  6847  f1oresrab  7109  fsn  7117  f1ounsn  7256  fveqf1o  7286  isoeq1  7301  f1oexbi  7909  oacomf1o  8534  mapsnd  8868  mapsnf1o3  8877  f1oen4g  8945  f1oen3g  8947  en0  8999  en0r  9001  ensn1  9002  en2sn  9022  en2prd  9028  xpcomf1o  9038  omf1o  9052  enfixsn  9058  domss2  9108  ssfiALT  9142  php3  9177  isinf  9209  oef1o  9653  cnfcom  9655  cnfcom3  9659  infxpenc  9974  ackbij2lem2  10195  ackbij2  10198  canthp1lem2  10611  pwfseqlem5  10621  seqf1olem2  14055  seqf1o  14056  hasheqf1oi  14364  hashf1rn  14365  hasheqf1od  14366  hashfacen  14467  wrd2f1tovbij  14973  s7f1o  14979  summo  15744  fsum  15747  ackbijnn  15858  prodmo  15966  fprod  15971  sadcaddlem  16491  unbenlem  16944  setcinv  18123  equivestrcsetc  18184  isgim  19302  symgval  19411  elsymgbas2  19413  symg1bas  19431  cayleyth  19455  gsumval3eu  19944  gsumval3lem1  19945  gsumval3lem2  19946  islmim  21126  uvcendim  21896  coe1mul2lem2  22328  mdet0f1o  22650  resinf1o  26598  efif1olem4  26607  logf1o  26626  relogf1o  26628  dvlog  26713  2lgslem1  27455  isismt  28700  nbusgrf1o1  29568  cusgrfilem3  29655  wwlksnextbij  30099  wlksnwwlknvbij  30105  clwwlkvbij  30312  hoif  31954  rabfodom  32701  fresf1o  32830  fpwrelmapffs  32933  fzo0pmtrlast  33269  pmtridf1o  33271  cycpmconjslem2  33332  1arithidomlem1  33728  1arithidom  33730  eulerpartlem1  34661  eulerpartgbij  34666  eulerpart  34676  derangenlem  35518  subfacp1lem2a  35527  subfacp1lem3  35529  subfacp1lem5  35531  subfacp1lem6  35532  subfacp1  35533  f1omptsn  37828  poimirlem3  38119  poimirlem4  38120  poimirlem5  38121  poimirlem6  38122  poimirlem7  38123  poimirlem8  38124  poimirlem9  38125  poimirlem10  38126  poimirlem11  38127  poimirlem12  38128  poimirlem13  38129  poimirlem14  38130  poimirlem15  38131  poimirlem16  38132  poimirlem17  38133  poimirlem18  38134  poimirlem19  38135  poimirlem20  38136  poimirlem21  38137  poimirlem22  38138  poimirlem25  38141  poimirlem26  38142  poimirlem27  38143  poimirlem29  38145  poimirlem31  38147  isismty  38297  isrngoiso  38474  islaut  40704  ispautN  40720  aks6d1c2  42744  sticksstones4  42763  sticksstones20  42780  eldioph2lem1  43338  pwfi2f1o  43670  rfovcnvf1od  44577  clsneif1o  44677  neicvgf1o  44687  nregmodelf1o  45588  3f1oss1  47666  fundcmpsurbijinjpreimafv  48010  sprbisymrel  48102  prproropen  48111  grimidvtxedg  48504  grimcnv  48507  grimco  48508  isuspgrim0  48513  gricushgr  48536  ushggricedg  48546  uhgrimisgrgric  48550  isgrtri  48562  isubgr3stgrlem3  48587  isubgr3stgr  48594  isgrlim  48601  uspgrlim  48611  grlicref  48631  grlicsym  48632  grlictr  48634  uspgrbispr  48770  uspgrbisymrelALT  48774  1aryenef  49264  2aryenef  49275  rrx2xpreen  49338  thincciso  50071  thinccisod  50072