Theorem f1oeq3d 6779

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 6772	. 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 1540  –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-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  resdif  6803  f1osng  6823  f1oresrab  7081  fveqf1o  7259  isoini2  7296  oacomf1o  8506  mapsnf1o  8889  domss2  9077  dif1enlem  9097  dif1enlemOLD  9098  infn0  9227  wemapwe  9626  oef1o  9627  cnfcomlem  9628  cnfcom3  9633  cnfcom3clem  9634  infxpenc  9947  infxpenc2lem1  9948  infxpenc2  9951  ackbij2lem2  10168  hsmexlem1  10355  fsumss  15667  fsumcnv  15715  fprodss  15890  fprodcnv  15925  pwssnf1o  17437  catcisolem  18052  equivestrcsetc  18093  yoniso  18226  gsumpropd  18587  gsumpropd2lem  18588  xpsmnd  18686  xpsgrp  18973  ghmqusker  19201  gsumval3lem1  19819  gsumval3lem2  19820  gsumcom2  19889  xpsrngd  20099  xpsringd  20252  rngqiprngim  21246  coe1mul2lem2  22187  scmatrngiso  22456  m2cpmrngiso  22678  cncfcnvcn  24852  isismt  28514  usgrf1oedg  29187  wlkiswwlks2lem5  29853  clwwlkvbij  30092  eupthres  30194  eupthp1  30195  cycpmconjvlem  33113  tocyccntz  33116  idomsubr  33275  dimkerim  33616  prodeq12sdv  36199  cbvsumdavw2  36276  cbvproddavw2  36277  poimirlem4  37611  poimirlem9  37616  rngoisoval  37964  frlmsnic  42521  sge0f1o  46373  nnfoctbdj  46447  3f1oss1  47069  f1oresf1o  47284  grimidvtxedg  47878  ushggricedg  47920  uhgrimisgrgric  47924  isubgr3stgrlem3  47960  uptrlem1  49192  uptrar  49198  uptr2  49203  oduoppcciso  49548