Theorem f1oeq1 6788

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 6751	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6768	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6518	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6518	. 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 6508  –onto→wfo 6509  –1-1-onto→wf1o 6510

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1oeq123d  6794  f1oeq1d  6795  f1ocnvb  6813  resin  6822  f1ovi  6839  f1oresrab  7099  fsn  7107  f1ounsn  7247  fveqf1o  7277  isoeq1  7292  f1oexbi  7904  oacomf1o  8529  mapsnd  8859  mapsnf1o3  8868  f1oen4g  8936  f1oen3g  8938  en0  8989  en0r  8991  ensn1  8992  en2sn  9012  en2prd  9019  xpcomf1o  9030  omf1o  9044  enfixsn  9050  domss2  9100  ssfiALT  9138  php3  9173  isinf  9207  isinfOLD  9208  oef1o  9651  cnfcom  9653  cnfcom3  9657  infxpenc  9971  ackbij2lem2  10192  ackbij2  10195  canthp1lem2  10606  pwfseqlem5  10616  seqf1olem2  14007  seqf1o  14008  hasheqf1oi  14316  hashf1rn  14317  hasheqf1od  14318  hashfacen  14419  wrd2f1tovbij  14926  s7f1o  14932  summo  15683  fsum  15686  ackbijnn  15794  prodmo  15902  fprod  15907  sadcaddlem  16427  unbenlem  16879  setcinv  18052  equivestrcsetc  18113  isgim  19194  symgval  19301  elsymgbas2  19303  symg1bas  19321  cayleyth  19345  gsumval3eu  19834  gsumval3lem1  19835  gsumval3lem2  19836  islmim  20969  uvcendim  21756  coe1mul2lem2  22154  mdet0f1o  22480  resinf1o  26445  efif1olem4  26454  logf1o  26473  relogf1o  26475  dvlog  26560  2lgslem1  27305  isismt  28461  nbusgrf1o1  29297  cusgrfilem3  29385  wwlksnextbij  29832  wlksnwwlknvbij  29838  clwwlkvbij  30042  hoif  31683  rabfodom  32434  fresf1o  32555  fpwrelmapffs  32657  fzo0pmtrlast  33049  pmtridf1o  33051  cycpmconjslem2  33112  1arithidomlem1  33506  1arithidom  33508  eulerpartlem1  34358  eulerpartgbij  34363  eulerpart  34373  derangenlem  35158  subfacp1lem2a  35167  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  subfacp1  35173  f1omptsn  37325  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  isismty  37795  isrngoiso  37972  islaut  40077  ispautN  40093  aks6d1c2  42118  sticksstones4  42137  sticksstones20  42154  eldioph2lem1  42748  pwfi2f1o  43085  rfovcnvf1od  43993  clsneif1o  44093  neicvgf1o  44103  nregmodelf1o  45005  3f1oss1  47076  fundcmpsurbijinjpreimafv  47408  sprbisymrel  47500  prproropen  47509  grimidvtxedg  47885  grimcnv  47888  grimco  47889  isuspgrim0  47894  gricushgr  47917  ushggricedg  47927  uhgrimisgrgric  47931  isgrtri  47942  isubgr3stgrlem3  47967  isubgr3stgr  47974  isgrlim  47981  uspgrlim  47991  grlicref  48004  grlicsym  48005  grlictr  48007  uspgrbispr  48139  uspgrbisymrelALT  48143  1aryenef  48634  2aryenef  48645  rrx2xpreen  48708  thincciso  49442  thinccisod  49443