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  18048  equivestrcsetc  18089  yoniso  18222  gsumpropd  18581  gsumpropd2lem  18582  xpsmnd  18680  xpsgrp  18967  ghmqusker  19195  gsumval3lem1  19811  gsumval3lem2  19812  gsumcom2  19881  xpsrngd  20064  xpsringd  20217  rngqiprngim  21190  coe1mul2lem2  22130  scmatrngiso  22399  m2cpmrngiso  22621  cncfcnvcn  24795  isismt  28437  usgrf1oedg  29110  wlkiswwlks2lem5  29776  clwwlkvbij  30015  eupthres  30117  eupthp1  30118  cycpmconjvlem  33071  tocyccntz  33074  idomsubr  33232  dimkerim  33596  prodeq12sdv  36179  cbvsumdavw2  36256  cbvproddavw2  36257  poimirlem4  37591  poimirlem9  37596  rngoisoval  37944  frlmsnic  42501  sge0f1o  46353  nnfoctbdj  46427  3f1oss1  47049  f1oresf1o  47264  grimidvtxedg  47858  ushggricedg  47900  uhgrimisgrgric  47904  isubgr3stgrlem3  47940  uptrlem1  49172  uptrar  49178  uptr2  49183  oduoppcciso  49528