Theorem f1oeq1 6751

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 6714	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
2		foeq1 6731	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐺:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–onto→𝐵)))
4		df-f1o 6488	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6488	. 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 1541  –1-1→wf1 6478  –onto→wfo 6479  –1-1-onto→wf1o 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1oeq123d  6757  f1oeq1d  6758  f1ocnvb  6776  resin  6785  f1ovi  6802  f1oresrab  7060  fsn  7068  f1ounsn  7206  fveqf1o  7236  isoeq1  7251  f1oexbi  7858  oacomf1o  8480  mapsnd  8810  mapsnf1o3  8819  f1oen4g  8887  f1oen3g  8889  en0  8940  en0r  8942  ensn1  8943  en2sn  8963  en2prd  8969  xpcomf1o  8979  omf1o  8993  enfixsn  8999  domss2  9049  ssfiALT  9083  php3  9118  isinf  9149  oef1o  9588  cnfcom  9590  cnfcom3  9594  infxpenc  9909  ackbij2lem2  10130  ackbij2  10133  canthp1lem2  10544  pwfseqlem5  10554  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  19174  symgval  19283  elsymgbas2  19285  symg1bas  19303  cayleyth  19327  gsumval3eu  19816  gsumval3lem1  19817  gsumval3lem2  19818  islmim  20996  uvcendim  21784  coe1mul2lem2  22182  mdet0f1o  22508  resinf1o  26472  efif1olem4  26481  logf1o  26500  relogf1o  26502  dvlog  26587  2lgslem1  27332  isismt  28512  nbusgrf1o1  29348  cusgrfilem3  29436  wwlksnextbij  29880  wlksnwwlknvbij  29886  clwwlkvbij  30093  hoif  31734  rabfodom  32485  fresf1o  32613  fpwrelmapffs  32717  fzo0pmtrlast  33061  pmtridf1o  33063  cycpmconjslem2  33124  1arithidomlem1  33500  1arithidom  33502  eulerpartlem1  34380  eulerpartgbij  34385  eulerpart  34395  derangenlem  35215  subfacp1lem2a  35224  subfacp1lem3  35226  subfacp1lem5  35228  subfacp1lem6  35229  subfacp1  35230  f1omptsn  37379  poimirlem3  37671  poimirlem4  37672  poimirlem5  37673  poimirlem6  37674  poimirlem7  37675  poimirlem8  37676  poimirlem9  37677  poimirlem10  37678  poimirlem11  37679  poimirlem12  37680  poimirlem13  37681  poimirlem14  37682  poimirlem15  37683  poimirlem16  37684  poimirlem17  37685  poimirlem18  37686  poimirlem19  37687  poimirlem20  37688  poimirlem21  37689  poimirlem22  37690  poimirlem25  37693  poimirlem26  37694  poimirlem27  37695  poimirlem29  37697  poimirlem31  37699  isismty  37849  isrngoiso  38026  islaut  40130  ispautN  40146  aks6d1c2  42171  sticksstones4  42190  sticksstones20  42207  eldioph2lem1  42801  pwfi2f1o  43137  rfovcnvf1od  44045  clsneif1o  44145  neicvgf1o  44155  nregmodelf1o  45056  3f1oss1  47114  fundcmpsurbijinjpreimafv  47446  sprbisymrel  47538  prproropen  47547  grimidvtxedg  47924  grimcnv  47927  grimco  47928  isuspgrim0  47933  gricushgr  47956  ushggricedg  47966  uhgrimisgrgric  47970  isgrtri  47982  isubgr3stgrlem3  48007  isubgr3stgr  48014  isgrlim  48021  uspgrlim  48031  grlicref  48051  grlicsym  48052  grlictr  48054  uspgrbispr  48190  uspgrbisymrelALT  48194  1aryenef  48685  2aryenef  48696  rrx2xpreen  48759  thincciso  49493  thinccisod  49494