Theorem f1oeq1 6836

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 6799	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6816	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6568	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6568	. 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 6558  –onto→wfo 6559  –1-1-onto→wf1o 6560

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is referenced by:  f1oeq123d  6842  f1oeq1d  6843  f1ocnvb  6861  resin  6870  f1ovi  6887  f1oresrab  7147  fsn  7155  f1ounsn  7292  fveqf1o  7322  isoeq1  7337  f1oexbi  7950  oacomf1o  8603  mapsnd  8926  mapsnf1o3  8935  f1oen4g  9005  f1oen3g  9007  en0  9058  en0r  9060  ensn1  9061  en2sn  9081  en2prd  9088  xpcomf1o  9101  omf1o  9115  enfixsn  9121  domss2  9176  ssfiALT  9214  php3  9249  php3OLD  9261  isinf  9296  isinfOLD  9297  oef1o  9738  cnfcom  9740  cnfcom3  9744  infxpenc  10058  ackbij2lem2  10279  ackbij2  10282  canthp1lem2  10693  pwfseqlem5  10703  seqf1olem2  14083  seqf1o  14084  hasheqf1oi  14390  hashf1rn  14391  hasheqf1od  14392  hashfacen  14493  wrd2f1tovbij  14999  s7f1o  15005  summo  15753  fsum  15756  ackbijnn  15864  prodmo  15972  fprod  15977  sadcaddlem  16494  unbenlem  16946  setcinv  18135  equivestrcsetc  18197  isgim  19280  symgval  19388  elsymgbas2  19390  symg1bas  19408  cayleyth  19433  gsumval3eu  19922  gsumval3lem1  19923  gsumval3lem2  19924  islmim  21061  uvcendim  21867  coe1mul2lem2  22271  mdet0f1o  22599  resinf1o  26578  efif1olem4  26587  logf1o  26606  relogf1o  26608  dvlog  26693  2lgslem1  27438  isismt  28542  nbusgrf1o1  29387  cusgrfilem3  29475  wwlksnextbij  29922  wlksnwwlknvbij  29928  clwwlkvbij  30132  hoif  31773  rabfodom  32524  fresf1o  32641  fpwrelmapffs  32745  fzo0pmtrlast  33112  pmtridf1o  33114  cycpmconjslem2  33175  1arithidomlem1  33563  1arithidom  33565  eulerpartlem1  34369  eulerpartgbij  34374  eulerpart  34384  derangenlem  35176  subfacp1lem2a  35185  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  subfacp1  35191  f1omptsn  37338  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem31  37658  isismty  37808  isrngoiso  37985  islaut  40085  ispautN  40101  aks6d1c2  42131  sticksstones4  42150  sticksstones20  42167  eldioph2lem1  42771  pwfi2f1o  43108  rfovcnvf1od  44017  clsneif1o  44117  neicvgf1o  44127  3f1oss1  47087  fundcmpsurbijinjpreimafv  47394  sprbisymrel  47486  prproropen  47495  isuspgrim0  47872  uspgrimprop  47873  grimidvtxedg  47876  grimcnv  47879  grimco  47880  gricushgr  47886  ushggricedg  47896  uhgrimisgrgric  47899  isgrtri  47910  isubgr3stgrlem3  47935  isubgr3stgr  47942  isgrlim  47949  uspgrlim  47959  grlicref  47972  grlicsym  47973  grlictr  47975  uspgrbispr  48067  uspgrbisymrelALT  48071  1aryenef  48566  2aryenef  48577  rrx2xpreen  48640  thincciso  49102  thinccisod  49103