Theorem f1oeq1 6812

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 6773	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6792	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6547	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6547	. 2 ⊢ (𝐺:𝐴–1-1-onto→𝐵 ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  –1-1→wf1 6537  –onto→wfo 6538  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1oeq123d  6818  f1oeq1d  6819  f1ocnvb  6838  resin  6847  f1ovi  6865  f1oresrab  7127  fsn  7135  f1ounsn  7279  fveqf1o  7309  isoeq1  7324  f1oexbi  7931  oacomf1o  8556  mapsnd  8890  mapsnf1o3  8899  f1oen4g  8967  f1oen3g  8969  en0  9021  en0r  9023  ensn1  9024  en2sn  9045  en2prd  9051  xpcomf1o  9061  omf1o  9075  enfixsn  9081  domss2  9131  ssfiALT  9165  php3  9200  isinf  9232  oef1o  9674  cnfcom  9676  cnfcom3  9680  infxpenc  10018  ackbij2lem2  10238  ackbij2  10241  canthp1lem2  10653  pwfseqlem5  10663  seqf1olem2  14096  seqf1o  14097  hasheqf1oi  14405  hashf1rn  14406  hasheqf1od  14407  hashfacen  14509  wrd2f1tovbij  15021  s7f1o  15027  summo  15791  fsum  15794  ackbijnn  15905  prodmo  16013  fprod  16018  sadcaddlem  16537  unbenlem  16990  setcinv  18169  equivestrcsetc  18230  isgim  19376  symgval  19485  elsymgbas2  19487  symg1bas  19505  cayleyth  19529  gsumval3eu  20018  gsumval3lem1  20019  gsumval3lem2  20020  rimval  20628  islmim  21233  uvcendim  22047  coe1mul2lem2  22479  mdet0f1o  22800  resinf1o  26752  efif1olem4  26761  logf1o  26780  relogf1o  26782  dvlog  26867  2lgslem1  27609  isismt  28854  nbusgrf1o1  29778  cusgrfilem3  29865  wwlksnextbij  30318  wlksnwwlknvbij  30324  clwwlkvbij  30531  hoif  32177  rabfodom  32922  fresf1o  33047  fpwrelmapffs  33149  fzo0pmtrlast  33476  pmtridf1o  33478  cycpmconjslem2  33539  1arithidomlem1  33889  1arithidom  33891  eulerpartlem1  34822  eulerpartgbij  34827  eulerpart  34837  derangenlem  35700  subfacp1lem2a  35709  subfacp1lem3  35711  subfacp1lem5  35713  subfacp1lem6  35714  subfacp1  35715  f1omptsn  38040  poimirlem3  38331  poimirlem4  38332  poimirlem5  38333  poimirlem6  38334  poimirlem7  38335  poimirlem8  38336  poimirlem9  38337  poimirlem10  38338  poimirlem11  38339  poimirlem12  38340  poimirlem13  38341  poimirlem14  38342  poimirlem15  38343  poimirlem16  38344  poimirlem17  38345  poimirlem18  38346  poimirlem19  38347  poimirlem20  38348  poimirlem21  38349  poimirlem22  38350  poimirlem25  38353  poimirlem26  38354  poimirlem27  38355  poimirlem29  38357  poimirlem31  38359  isismty  38510  isrngoiso  38687  islaut  40915  ispautN  40931  aks6d1c2  42955  sticksstones4  42974  sticksstones20  42991  eldioph2lem1  43549  pwfi2f1o  43881  rfovcnvf1od  44788  clsneif1o  44888  neicvgf1o  44898  nregmodelf1o  45782  3f1oss1  47870  fundcmpsurbijinjpreimafv  48214  sprbisymrel  48306  prproropen  48315  grimidvtxedg  48708  grimcnv  48711  grimco  48712  isuspgrim0  48717  gricushgr  48740  ushggricedg  48750  uhgrimisgrgric  48754  isgrtri  48766  isubgr3stgrlem3  48791  isubgr3stgr  48798  isgrlim  48805  uspgrlim  48815  grlicref  48835  grlicsym  48836  grlictr  48838  uspgrbispr  48974  uspgrbisymrelALT  48978  1aryenef  49482  2aryenef  49493  rrx2xpreen  49556  thincciso  50288  thinccisod  50289