Theorem f1oeq3d 6587

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 6581	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  –1-1-onto→wf1o 6323

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331

This theorem is referenced by:  resdif  6610  f1osng  6630  f1oresrab  6866  fveqf1o  7037  isoini2  7071  oacomf1o  8174  mapsnf1o  8486  domss2  8660  wemapwe  9144  oef1o  9145  cnfcomlem  9146  cnfcom3  9151  cnfcom3clem  9152  infxpenc  9429  infxpenc2lem1  9430  infxpenc2  9433  ackbij2lem2  9651  hsmexlem1  9837  fsumss  15074  fsumcnv  15120  fprodss  15294  fprodcnv  15329  pwssnf1o  16763  catcisolem  17358  equivestrcsetc  17394  yoniso  17527  gsumpropd  17880  gsumpropd2lem  17881  xpsmnd  17943  xpsgrp  18210  gsumval3lem1  19018  gsumval3lem2  19019  gsumcom2  19088  coe1mul2lem2  20897  scmatrngiso  21141  m2cpmrngiso  21363  cncfcnvcn  23530  isismt  26328  usgrf1oedg  26997  wlkiswwlks2lem5  27659  clwwlkvbij  27898  eupthres  28000  eupthp1  28001  cycpmconjvlem  30833  tocyccntz  30836  dimkerim  31111  poimirlem9  35066  rngoisoval  35415  frlmsnic  39453  sge0f1o  43021  nnfoctbdj  43095  f1oresf1o  43846  ushrisomgr  44359