Theorem f1oeq1 6770

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 6733	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6750	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6506	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6506	. 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 6496  –onto→wfo 6497  –1-1-onto→wf1o 6498

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1oeq123d  6776  f1oeq1d  6777  f1ocnvb  6795  resin  6804  f1ovi  6821  f1oresrab  7081  fsn  7089  f1ounsn  7229  fveqf1o  7259  isoeq1  7274  f1oexbi  7884  oacomf1o  8506  mapsnd  8836  mapsnf1o3  8845  f1oen4g  8913  f1oen3g  8915  en0  8966  en0r  8968  ensn1  8969  en2sn  8989  en2prd  8996  xpcomf1o  9007  omf1o  9021  enfixsn  9027  domss2  9077  ssfiALT  9115  php3  9150  isinf  9183  isinfOLD  9184  oef1o  9627  cnfcom  9629  cnfcom3  9633  infxpenc  9947  ackbij2lem2  10168  ackbij2  10171  canthp1lem2  10582  pwfseqlem5  10592  seqf1olem2  13983  seqf1o  13984  hasheqf1oi  14292  hashf1rn  14293  hasheqf1od  14294  hashfacen  14395  wrd2f1tovbij  14902  s7f1o  14908  summo  15659  fsum  15662  ackbijnn  15770  prodmo  15878  fprod  15883  sadcaddlem  16403  unbenlem  16855  setcinv  18028  equivestrcsetc  18089  isgim  19170  symgval  19277  elsymgbas2  19279  symg1bas  19297  cayleyth  19321  gsumval3eu  19810  gsumval3lem1  19811  gsumval3lem2  19812  islmim  20945  uvcendim  21732  coe1mul2lem2  22130  mdet0f1o  22456  resinf1o  26421  efif1olem4  26430  logf1o  26449  relogf1o  26451  dvlog  26536  2lgslem1  27281  isismt  28437  nbusgrf1o1  29273  cusgrfilem3  29361  wwlksnextbij  29805  wlksnwwlknvbij  29811  clwwlkvbij  30015  hoif  31656  rabfodom  32407  fresf1o  32528  fpwrelmapffs  32630  fzo0pmtrlast  33022  pmtridf1o  33024  cycpmconjslem2  33085  1arithidomlem1  33479  1arithidom  33481  eulerpartlem1  34331  eulerpartgbij  34336  eulerpart  34346  derangenlem  35131  subfacp1lem2a  35140  subfacp1lem3  35142  subfacp1lem5  35144  subfacp1lem6  35145  subfacp1  35146  f1omptsn  37298  poimirlem3  37590  poimirlem4  37591  poimirlem5  37592  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem9  37596  poimirlem10  37597  poimirlem11  37598  poimirlem12  37599  poimirlem13  37600  poimirlem14  37601  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem29  37616  poimirlem31  37618  isismty  37768  isrngoiso  37945  islaut  40050  ispautN  40066  aks6d1c2  42091  sticksstones4  42110  sticksstones20  42127  eldioph2lem1  42721  pwfi2f1o  43058  rfovcnvf1od  43966  clsneif1o  44066  neicvgf1o  44076  nregmodelf1o  44978  3f1oss1  47049  fundcmpsurbijinjpreimafv  47381  sprbisymrel  47473  prproropen  47482  grimidvtxedg  47858  grimcnv  47861  grimco  47862  isuspgrim0  47867  gricushgr  47890  ushggricedg  47900  uhgrimisgrgric  47904  isgrtri  47915  isubgr3stgrlem3  47940  isubgr3stgr  47947  isgrlim  47954  uspgrlim  47964  grlicref  47977  grlicsym  47978  grlictr  47980  uspgrbispr  48112  uspgrbisymrelALT  48116  1aryenef  48607  2aryenef  48618  rrx2xpreen  48681  thincciso  49415  thinccisod  49416