Theorem f1oeq3d 6764

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  resdif  6788  f1osng  6809  f1oresrab  7069  fveqf1o  7246  isoini2  7283  oacomf1o  8490  mapsnf1o  8877  domss2  9064  dif1enlem  9084  infn0  9202  wemapwe  9609  oef1o  9610  cnfcomlem  9611  cnfcom3  9616  cnfcom3clem  9617  infxpenc  9931  infxpenc2lem1  9932  infxpenc2  9935  ackbij2lem2  10152  hsmexlem1  10339  fsumss  15678  fsumcnv  15726  fprodss  15904  fprodcnv  15939  pwssnf1o  17453  catcisolem  18068  equivestrcsetc  18109  yoniso  18242  gsumpropd  18637  gsumpropd2lem  18638  xpsmnd  18736  xpsgrp  19026  ghmqusker  19253  gsumval3lem1  19871  gsumval3lem2  19872  gsumcom2  19941  xpsrngd  20151  xpsringd  20303  rngqiprngim  21297  coe1mul2lem2  22254  scmatrngiso  22519  m2cpmrngiso  22741  cncfcnvcn  24910  isismt  28620  usgrf1oedg  29294  wlkiswwlks2lem5  29959  clwwlkvbij  30201  eupthres  30303  eupthp1  30304  f1oeq3dd  32721  cycpmconjvlem  33222  tocyccntz  33225  idomsubr  33393  dimkerim  33811  prodeq12sdv  36446  cbvsumdavw2  36523  cbvproddavw2  36524  poimirlem4  37991  poimirlem9  37996  rngoisoval  38344  frlmsnic  43026  sge0f1o  46825  nnfoctbdj  46899  3f1oss1  47538  f1oresf1o  47753  grimidvtxedg  48376  ushggricedg  48418  uhgrimisgrgric  48422  isubgr3stgrlem3  48459  uptrlem1  49700  uptrar  49706  uptr2  49711  oduoppcciso  50056