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 6569	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
5		df-f1o 6569	. 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 1536  –1-1→wf1 6559  –onto→wfo 6560  –1-1-onto→wf1o 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569

This theorem is referenced by:  f1oeq123d  6842  f1oeq1d  6843  f1ocnvb  6861  resin  6870  f1ovi  6887  f1oresrab  7146  fsn  7154  f1ounsn  7291  fveqf1o  7321  isoeq1  7336  f1oexbi  7950  oacomf1o  8601  mapsnd  8924  mapsnf1o3  8933  f1oen4g  9003  f1oen3g  9005  en0  9056  en0r  9058  ensn1  9059  en2sn  9079  en2prd  9086  xpcomf1o  9099  omf1o  9113  enfixsn  9119  domss2  9174  ssfiALT  9212  php3  9246  php3OLD  9258  isinf  9293  isinfOLD  9294  oef1o  9735  cnfcom  9737  cnfcom3  9741  infxpenc  10055  ackbij2lem2  10276  ackbij2  10279  canthp1lem2  10690  pwfseqlem5  10700  seqf1olem2  14079  seqf1o  14080  hasheqf1oi  14386  hashf1rn  14387  hasheqf1od  14388  hashfacen  14489  wrd2f1tovbij  14995  s7f1o  15001  summo  15749  fsum  15752  ackbijnn  15860  prodmo  15968  fprod  15973  sadcaddlem  16490  unbenlem  16941  setcinv  18143  equivestrcsetc  18207  isgim  19292  symgval  19402  elsymgbas2  19404  symg1bas  19422  cayleyth  19447  gsumval3eu  19936  gsumval3lem1  19937  gsumval3lem2  19938  islmim  21078  uvcendim  21884  coe1mul2lem2  22286  mdet0f1o  22614  resinf1o  26592  efif1olem4  26601  logf1o  26620  relogf1o  26622  dvlog  26707  2lgslem1  27452  isismt  28556  nbusgrf1o1  29401  cusgrfilem3  29489  wwlksnextbij  29931  wlksnwwlknvbij  29937  clwwlkvbij  30141  hoif  31782  rabfodom  32532  fresf1o  32647  fpwrelmapffs  32751  fzo0pmtrlast  33094  pmtridf1o  33096  cycpmconjslem2  33157  1arithidomlem1  33542  1arithidom  33544  eulerpartlem1  34348  eulerpartgbij  34353  eulerpart  34363  derangenlem  35155  subfacp1lem2a  35164  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  subfacp1  35170  f1omptsn  37319  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem31  37637  isismty  37787  isrngoiso  37964  islaut  40065  ispautN  40081  aks6d1c2  42111  sticksstones4  42130  sticksstones20  42147  eldioph2lem1  42747  pwfi2f1o  43084  rfovcnvf1od  43993  clsneif1o  44093  neicvgf1o  44103  3f1oss1  47024  fundcmpsurbijinjpreimafv  47331  sprbisymrel  47423  prproropen  47432  isuspgrim0  47809  uspgrimprop  47810  grimidvtxedg  47813  grimcnv  47816  grimco  47817  gricushgr  47823  ushggricedg  47833  uhgrimisgrgric  47836  isgrtri  47847  isubgr3stgrlem3  47870  isubgr3stgr  47877  isgrlim  47884  uspgrlim  47894  grlicref  47907  grlicsym  47908  grlictr  47910  uspgrbispr  47994  uspgrbisymrelALT  47998  1aryenef  48494  2aryenef  48505  rrx2xpreen  48568  thincciso  48848  thinccisod  48849