Theorem f1oeq3d 6769

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
f1oeq3d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
f1oeq3d	⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Proof of Theorem f1oeq3d

Step	Hyp	Ref	Expression
1		f1oeq3d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq3 6762	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  –1-1-onto→wf1o 6489

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-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  resdif  6793  f1osng  6814  f1oresrab  7070  fveqf1o  7246  isoini2  7283  oacomf1o  8490  mapsnf1o  8875  domss2  9062  dif1enlem  9082  infn0  9200  wemapwe  9604  oef1o  9605  cnfcomlem  9606  cnfcom3  9611  cnfcom3clem  9612  infxpenc  9926  infxpenc2lem1  9927  infxpenc2  9930  ackbij2lem2  10147  hsmexlem1  10334  fsumss  15646  fsumcnv  15694  fprodss  15869  fprodcnv  15904  pwssnf1o  17417  catcisolem  18032  equivestrcsetc  18073  yoniso  18206  gsumpropd  18601  gsumpropd2lem  18602  xpsmnd  18700  xpsgrp  18987  ghmqusker  19214  gsumval3lem1  19832  gsumval3lem2  19833  gsumcom2  19902  xpsrngd  20112  xpsringd  20266  rngqiprngim  21257  coe1mul2lem2  22208  scmatrngiso  22478  m2cpmrngiso  22700  cncfcnvcn  24873  isismt  28555  usgrf1oedg  29229  wlkiswwlks2lem5  29895  clwwlkvbij  30137  eupthres  30239  eupthp1  30240  f1oeq3dd  32656  cycpmconjvlem  33172  tocyccntz  33175  idomsubr  33340  dimkerim  33733  prodeq12sdv  36361  cbvsumdavw2  36438  cbvproddavw2  36439  poimirlem4  37764  poimirlem9  37769  rngoisoval  38117  frlmsnic  42737  sge0f1o  46568  nnfoctbdj  46642  3f1oss1  47263  f1oresf1o  47478  grimidvtxedg  48073  ushggricedg  48115  uhgrimisgrgric  48119  isubgr3stgrlem3  48156  uptrlem1  49397  uptrar  49403  uptr2  49408  oduoppcciso  49753