Theorem f1oeq1 6752

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 6715	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6732	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6489	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6489	. 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 6479  –onto→wfo 6480  –1-1-onto→wf1o 6481

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  f1oeq123d  6758  f1oeq1d  6759  f1ocnvb  6777  resin  6786  f1ovi  6803  f1oresrab  7061  fsn  7069  f1ounsn  7209  fveqf1o  7239  isoeq1  7254  f1oexbi  7861  oacomf1o  8483  mapsnd  8813  mapsnf1o3  8822  f1oen4g  8890  f1oen3g  8892  en0  8943  en0r  8945  ensn1  8946  en2sn  8966  en2prd  8973  xpcomf1o  8983  omf1o  8997  enfixsn  9003  domss2  9053  ssfiALT  9088  php3  9123  isinf  9154  oef1o  9594  cnfcom  9596  cnfcom3  9600  infxpenc  9912  ackbij2lem2  10133  ackbij2  10136  canthp1lem2  10547  pwfseqlem5  10557  seqf1olem2  13949  seqf1o  13950  hasheqf1oi  14258  hashf1rn  14259  hasheqf1od  14260  hashfacen  14361  wrd2f1tovbij  14867  s7f1o  14873  summo  15624  fsum  15627  ackbijnn  15735  prodmo  15843  fprod  15848  sadcaddlem  16368  unbenlem  16820  setcinv  17997  equivestrcsetc  18058  isgim  19141  symgval  19250  elsymgbas2  19252  symg1bas  19270  cayleyth  19294  gsumval3eu  19783  gsumval3lem1  19784  gsumval3lem2  19785  islmim  20966  uvcendim  21754  coe1mul2lem2  22152  mdet0f1o  22478  resinf1o  26443  efif1olem4  26452  logf1o  26471  relogf1o  26473  dvlog  26558  2lgslem1  27303  isismt  28479  nbusgrf1o1  29315  cusgrfilem3  29403  wwlksnextbij  29847  wlksnwwlknvbij  29853  clwwlkvbij  30057  hoif  31698  rabfodom  32449  fresf1o  32574  fpwrelmapffs  32677  fzo0pmtrlast  33034  pmtridf1o  33036  cycpmconjslem2  33097  1arithidomlem1  33472  1arithidom  33474  eulerpartlem1  34335  eulerpartgbij  34340  eulerpart  34350  derangenlem  35144  subfacp1lem2a  35153  subfacp1lem3  35155  subfacp1lem5  35157  subfacp1lem6  35158  subfacp1  35159  f1omptsn  37311  poimirlem3  37603  poimirlem4  37604  poimirlem5  37605  poimirlem6  37606  poimirlem7  37607  poimirlem8  37608  poimirlem9  37609  poimirlem10  37610  poimirlem11  37611  poimirlem12  37612  poimirlem13  37613  poimirlem14  37614  poimirlem15  37615  poimirlem16  37616  poimirlem17  37617  poimirlem18  37618  poimirlem19  37619  poimirlem20  37620  poimirlem21  37621  poimirlem22  37622  poimirlem25  37625  poimirlem26  37626  poimirlem27  37627  poimirlem29  37629  poimirlem31  37631  isismty  37781  isrngoiso  37958  islaut  40062  ispautN  40078  aks6d1c2  42103  sticksstones4  42122  sticksstones20  42139  eldioph2lem1  42733  pwfi2f1o  43069  rfovcnvf1od  43977  clsneif1o  44077  neicvgf1o  44087  nregmodelf1o  44989  3f1oss1  47059  fundcmpsurbijinjpreimafv  47391  sprbisymrel  47483  prproropen  47492  grimidvtxedg  47869  grimcnv  47872  grimco  47873  isuspgrim0  47878  gricushgr  47901  ushggricedg  47911  uhgrimisgrgric  47915  isgrtri  47927  isubgr3stgrlem3  47952  isubgr3stgr  47959  isgrlim  47966  uspgrlim  47976  grlicref  47996  grlicsym  47997  grlictr  47999  uspgrbispr  48135  uspgrbisymrelALT  48139  1aryenef  48630  2aryenef  48641  rrx2xpreen  48704  thincciso  49438  thinccisod  49439