Theorem f1oeq3d 6818

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is referenced by:  resdif  6843  f1osng  6864  f1oresrab  7124  fveqf1o  7301  isoini2  7338  oacomf1o  8549  mapsnf1o  8936  domss2  9123  dif1enlem  9143  infn0  9261  wemapwe  9665  oef1o  9666  cnfcomlem  9667  cnfcom3  9672  cnfcom3clem  9673  infxpenc  10001  infxpenc2lem1  10002  infxpenc2  10005  ackbij2lem2  10221  hsmexlem1  10409  fsumss  15775  fsumcnv  15823  fprodss  16001  fprodcnv  16036  pwssnf1o  17551  catcisolem  18166  equivestrcsetc  18207  yoniso  18340  gsumpropd  18735  gsumpropd2lem  18736  xpsmnd  18834  xpsgrp  19124  ghmqusker  19356  gsumval3lem1  19974  gsumval3lem2  19975  gsumcom2  20044  xpsrngd  20256  xpsringd  20413  rngqiprngim  21414  coe1mul2lem2  22397  scmatrngiso  22661  m2cpmrngiso  22883  cncfcnvcn  25052  isismt  28768  usgrf1oedg  29497  wlkiswwlks2lem5  30162  clwwlkvbij  30404  eupthres  30506  eupthp1  30507  f1oeq3dd  32914  cycpmconjvlem  33401  tocyccntz  33404  idomsubr  33572  dimkerim  33961  prodeq12sdv  36618  cbvsumdavw2  36695  cbvproddavw2  36696  poimirlem4  38162  poimirlem9  38167  rngoisoval  38515  frlmsnic  43199  sge0f1o  46987  nnfoctbdj  47061  3f1oss1  47700  f1oresf1o  47915  grimidvtxedg  48538  ushggricedg  48580  uhgrimisgrgric  48584  isubgr3stgrlem3  48621  uptrlem1  49872  uptrar  49878  uptr2  49883  oduoppcciso  50228