Theorem f1oeq3d 6760

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 6753	. 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 1541  –1-1-onto→wf1o 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  resdif  6784  f1osng  6804  f1oresrab  7060  fveqf1o  7236  isoini2  7273  oacomf1o  8480  mapsnf1o  8863  domss2  9049  dif1enlem  9069  infn0  9186  wemapwe  9587  oef1o  9588  cnfcomlem  9589  cnfcom3  9594  cnfcom3clem  9595  infxpenc  9909  infxpenc2lem1  9910  infxpenc2  9913  ackbij2lem2  10130  hsmexlem1  10317  fsumss  15632  fsumcnv  15680  fprodss  15855  fprodcnv  15890  pwssnf1o  17402  catcisolem  18017  equivestrcsetc  18058  yoniso  18191  gsumpropd  18586  gsumpropd2lem  18587  xpsmnd  18685  xpsgrp  18972  ghmqusker  19199  gsumval3lem1  19817  gsumval3lem2  19818  gsumcom2  19887  xpsrngd  20097  xpsringd  20250  rngqiprngim  21241  coe1mul2lem2  22182  scmatrngiso  22451  m2cpmrngiso  22673  cncfcnvcn  24846  isismt  28512  usgrf1oedg  29185  wlkiswwlks2lem5  29851  clwwlkvbij  30093  eupthres  30195  eupthp1  30196  f1oeq3dd  32611  cycpmconjvlem  33110  tocyccntz  33113  idomsubr  33275  dimkerim  33640  prodeq12sdv  36260  cbvsumdavw2  36337  cbvproddavw2  36338  poimirlem4  37672  poimirlem9  37677  rngoisoval  38025  frlmsnic  42581  sge0f1o  46428  nnfoctbdj  46502  3f1oss1  47114  f1oresf1o  47329  grimidvtxedg  47924  ushggricedg  47966  uhgrimisgrgric  47970  isubgr3stgrlem3  48007  uptrlem1  49250  uptrar  49256  uptr2  49261  oduoppcciso  49606