Theorem f1oeq1 6806

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 6769	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6786	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6538	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6538	. 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 206   ∧ wa 395   = wceq 1540  –1-1→wf1 6528  –onto→wfo 6529  –1-1-onto→wf1o 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538

This theorem is referenced by:  f1oeq123d  6812  f1oeq1d  6813  f1ocnvb  6831  resin  6840  f1ovi  6857  f1oresrab  7117  fsn  7125  f1ounsn  7265  fveqf1o  7295  isoeq1  7310  f1oexbi  7924  oacomf1o  8577  mapsnd  8900  mapsnf1o3  8909  f1oen4g  8979  f1oen3g  8981  en0  9032  en0r  9034  ensn1  9035  en2sn  9055  en2prd  9062  xpcomf1o  9075  omf1o  9089  enfixsn  9095  domss2  9150  ssfiALT  9188  php3  9223  php3OLD  9233  isinf  9268  isinfOLD  9269  oef1o  9712  cnfcom  9714  cnfcom3  9718  infxpenc  10032  ackbij2lem2  10253  ackbij2  10256  canthp1lem2  10667  pwfseqlem5  10677  seqf1olem2  14060  seqf1o  14061  hasheqf1oi  14369  hashf1rn  14370  hasheqf1od  14371  hashfacen  14472  wrd2f1tovbij  14979  s7f1o  14985  summo  15733  fsum  15736  ackbijnn  15844  prodmo  15952  fprod  15957  sadcaddlem  16476  unbenlem  16928  setcinv  18103  equivestrcsetc  18164  isgim  19245  symgval  19352  elsymgbas2  19354  symg1bas  19372  cayleyth  19396  gsumval3eu  19885  gsumval3lem1  19886  gsumval3lem2  19887  islmim  21020  uvcendim  21807  coe1mul2lem2  22205  mdet0f1o  22531  resinf1o  26497  efif1olem4  26506  logf1o  26525  relogf1o  26527  dvlog  26612  2lgslem1  27357  isismt  28513  nbusgrf1o1  29349  cusgrfilem3  29437  wwlksnextbij  29884  wlksnwwlknvbij  29890  clwwlkvbij  30094  hoif  31735  rabfodom  32486  fresf1o  32609  fpwrelmapffs  32711  fzo0pmtrlast  33103  pmtridf1o  33105  cycpmconjslem2  33166  1arithidomlem1  33550  1arithidom  33552  eulerpartlem1  34399  eulerpartgbij  34404  eulerpart  34414  derangenlem  35193  subfacp1lem2a  35202  subfacp1lem3  35204  subfacp1lem5  35206  subfacp1lem6  35207  subfacp1  35208  f1omptsn  37355  poimirlem3  37647  poimirlem4  37648  poimirlem5  37649  poimirlem6  37650  poimirlem7  37651  poimirlem8  37652  poimirlem9  37653  poimirlem10  37654  poimirlem11  37655  poimirlem12  37656  poimirlem13  37657  poimirlem14  37658  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem18  37662  poimirlem19  37663  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem25  37669  poimirlem26  37670  poimirlem27  37671  poimirlem29  37673  poimirlem31  37675  isismty  37825  isrngoiso  38002  islaut  40102  ispautN  40118  aks6d1c2  42143  sticksstones4  42162  sticksstones20  42179  eldioph2lem1  42783  pwfi2f1o  43120  rfovcnvf1od  44028  clsneif1o  44128  neicvgf1o  44138  3f1oss1  47104  fundcmpsurbijinjpreimafv  47421  sprbisymrel  47513  prproropen  47522  grimidvtxedg  47898  grimcnv  47901  grimco  47902  isuspgrim0  47907  gricushgr  47930  ushggricedg  47940  uhgrimisgrgric  47944  isgrtri  47955  isubgr3stgrlem3  47980  isubgr3stgr  47987  isgrlim  47994  uspgrlim  48004  grlicref  48017  grlicsym  48018  grlictr  48020  uspgrbispr  48126  uspgrbisymrelALT  48130  1aryenef  48625  2aryenef  48636  rrx2xpreen  48699  thincciso  49339  thinccisod  49340