Theorem f1oeq1 6713

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 6674	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6693	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6444	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6444	. 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 396   = wceq 1539  –1-1→wf1 6434  –onto→wfo 6435  –1-1-onto→wf1o 6436

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444

This theorem is referenced by:  f1oeq123d  6719  f1oeq1d  6720  f1ocnvb  6738  resin  6747  f1ovi  6764  f1oresrab  7008  fsn  7016  fveqf1o  7184  isoeq1  7197  f1oexbi  7784  oacomf1o  8405  mapsnd  8683  mapsnf1o3  8692  f1oen3g  8763  en0  8812  en0OLD  8813  en0r  8815  ensn1  8816  ensn1OLD  8817  en2sn  8840  en2snOLD  8841  xpcomf1o  8857  omf1o  8871  enfixsn  8877  domss2  8932  ssfiALT  8966  php3  9004  php3OLD  9016  isinf  9045  oef1o  9465  cnfcom  9467  cnfcom3  9471  infxpenc  9783  ackbij2lem2  10005  ackbij2  10008  canthp1lem2  10418  pwfseqlem5  10428  seqf1olem2  13772  seqf1o  13773  hasheqf1oi  14075  hashf1rn  14076  hasheqf1od  14077  hashfacen  14175  hashfacenOLD  14176  wrd2f1tovbij  14684  summo  15438  fsum  15441  ackbijnn  15549  prodmo  15655  fprod  15660  sadcaddlem  16173  unbenlem  16618  setcinv  17814  equivestrcsetc  17878  isgim  18887  symgval  18985  elsymgbas2  18989  symg1bas  19007  cayleyth  19032  gsumval3eu  19514  gsumval3lem1  19515  gsumval3lem2  19516  islmim  20333  uvcendim  21063  coe1mul2lem2  21448  mdet0f1o  21751  resinf1o  25701  efif1olem4  25710  logf1o  25729  relogf1o  25731  dvlog  25815  2lgslem1  26551  isismt  26904  nbusgrf1o1  27746  cusgrfilem3  27833  wwlksnextbij  28276  wlksnwwlknvbij  28282  clwwlkvbij  28486  hoif  30125  rabfodom  30860  fresf1o  30975  fpwrelmapffs  31078  pmtridf1o  31370  cycpmconjslem2  31431  eulerpartlem1  32343  eulerpartgbij  32348  eulerpart  32358  derangenlem  33142  subfacp1lem2a  33151  subfacp1lem3  33153  subfacp1lem5  33155  subfacp1lem6  33156  subfacp1  33157  f1omptsn  35517  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem31  35817  isismty  35968  isrngoiso  36145  islaut  38104  ispautN  38120  sticksstones4  40112  sticksstones20  40129  eldioph2lem1  40589  pwfi2f1o  40928  rfovcnvf1od  41619  clsneif1o  41721  neicvgf1o  41731  fundcmpsurbijinjpreimafv  44870  sprbisymrel  44962  prproropen  44971  isomgreqve  45288  isomushgr  45289  isomuspgrlem2  45296  isomgrsym  45299  isomgrtr  45302  ushrisomgr  45304  uspgrbispr  45324  uspgrbisymrelALT  45328  1aryenef  46002  2aryenef  46013  rrx2xpreen  46076  thincciso  46341