Theorem f1oeq3d 6821

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  resdif  6846  f1osng  6867  f1oresrab  7127  fveqf1o  7309  isoini2  7346  oacomf1o  8556  mapsnf1o  8943  domss2  9131  dif1enlem  9151  infn0  9269  wemapwe  9673  oef1o  9674  cnfcomlem  9675  cnfcom3  9680  cnfcom3clem  9681  infxpenc  10018  infxpenc2lem1  10019  infxpenc2  10022  ackbij2lem2  10238  hsmexlem1  10425  fsumss  15799  fsumcnv  15847  fprodss  16025  fprodcnv  16060  pwssnf1o  17574  catcisolem  18189  equivestrcsetc  18230  yoniso  18363  gsumpropd  18768  gsumpropd2lem  18769  xpsmnd  18872  xpsgrp  19169  ghmqusker  19401  gsumval3lem1  20019  gsumval3lem2  20020  gsumcom2  20089  xpsrngd  20301  xpsringd  20460  rngqiprngim  21494  coe1mul2lem2  22479  scmatrngiso  22743  m2cpmrngiso  22965  cncfcnvcn  25135  isismt  28854  usgrf1oedg  29615  wlkiswwlks2lem5  30289  clwwlkvbij  30531  eupthres  30637  eupthp1  30638  f1oeq3dd  33045  cycpmconjvlem  33525  tocyccntz  33528  idomsubr  33694  dimkerim  34081  prodeq12sdv  36787  cbvsumdavw2  36864  cbvproddavw2  36865  poimirlem4  38332  poimirlem9  38337  rngoisoval  38686  frlmsnic  43366  sge0f1o  47154  nnfoctbdj  47228  3f1oss1  47870  f1oresf1o  48085  grimidvtxedg  48708  ushggricedg  48750  uhgrimisgrgric  48754  isubgr3stgrlem3  48791  uptrlem1  50045  uptrar  50051  uptr2  50056  oduoppcciso  50401