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 1542  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  resdif  6803  f1osng  6824  f1oresrab  7082  fveqf1o  7258  isoini2  7295  oacomf1o  8502  mapsnf1o  8889  domss2  9076  dif1enlem  9096  infn0  9214  wemapwe  9618  oef1o  9619  cnfcomlem  9620  cnfcom3  9625  cnfcom3clem  9626  infxpenc  9940  infxpenc2lem1  9941  infxpenc2  9944  ackbij2lem2  10161  hsmexlem1  10348  fsumss  15660  fsumcnv  15708  fprodss  15883  fprodcnv  15918  pwssnf1o  17431  catcisolem  18046  equivestrcsetc  18087  yoniso  18220  gsumpropd  18615  gsumpropd2lem  18616  xpsmnd  18714  xpsgrp  19001  ghmqusker  19228  gsumval3lem1  19846  gsumval3lem2  19847  gsumcom2  19916  xpsrngd  20126  xpsringd  20280  rngqiprngim  21271  coe1mul2lem2  22222  scmatrngiso  22492  m2cpmrngiso  22714  cncfcnvcn  24887  isismt  28618  usgrf1oedg  29292  wlkiswwlks2lem5  29958  clwwlkvbij  30200  eupthres  30302  eupthp1  30303  f1oeq3dd  32719  cycpmconjvlem  33235  tocyccntz  33238  idomsubr  33403  dimkerim  33805  prodeq12sdv  36434  cbvsumdavw2  36511  cbvproddavw2  36512  poimirlem4  37875  poimirlem9  37880  rngoisoval  38228  frlmsnic  42910  sge0f1o  46740  nnfoctbdj  46814  3f1oss1  47435  f1oresf1o  47650  grimidvtxedg  48245  ushggricedg  48287  uhgrimisgrgric  48291  isubgr3stgrlem3  48328  uptrlem1  49569  uptrar  49575  uptr2  49580  oduoppcciso  49925