Theorem f1oeq3d 6705

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  –1-1-onto→wf1o 6425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3431  df-in 3893  df-ss 3903  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433

This theorem is referenced by:  resdif  6729  f1osng  6749  f1oresrab  6991  fveqf1o  7167  isoini2  7202  oacomf1o  8383  mapsnf1o  8714  domss2  8910  dif1enlem  8930  wemapwe  9442  oef1o  9443  cnfcomlem  9444  cnfcom3  9449  cnfcom3clem  9450  infxpenc  9784  infxpenc2lem1  9785  infxpenc2  9788  ackbij2lem2  10006  hsmexlem1  10192  fsumss  15447  fsumcnv  15495  fprodss  15668  fprodcnv  15703  pwssnf1o  17219  catcisolem  17835  equivestrcsetc  17879  yoniso  18013  gsumpropd  18372  gsumpropd2lem  18373  xpsmnd  18435  xpsgrp  18704  gsumval3lem1  19516  gsumval3lem2  19517  gsumcom2  19586  coe1mul2lem2  21449  scmatrngiso  21695  m2cpmrngiso  21917  cncfcnvcn  24098  isismt  26905  usgrf1oedg  27584  wlkiswwlks2lem5  28246  clwwlkvbij  28485  eupthres  28587  eupthp1  28588  cycpmconjvlem  31416  tocyccntz  31419  dimkerim  31716  poimirlem4  35789  poimirlem9  35794  rngoisoval  36143  frlmsnic  40271  sge0f1o  43901  nnfoctbdj  43975  f1oresf1o  44760  ushrisomgr  45271