Theorem f1oeq3d 6803

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  –1-1-onto→wf1o 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528

This theorem is referenced by:  resdif  6828  f1osng  6849  f1oresrab  7109  fveqf1o  7286  isoini2  7323  oacomf1o  8534  mapsnf1o  8921  domss2  9108  dif1enlem  9128  infn0  9246  wemapwe  9652  oef1o  9653  cnfcomlem  9654  cnfcom3  9659  cnfcom3clem  9660  infxpenc  9974  infxpenc2lem1  9975  infxpenc2  9978  ackbij2lem2  10195  hsmexlem1  10383  fsumss  15752  fsumcnv  15800  fprodss  15978  fprodcnv  16013  pwssnf1o  17528  catcisolem  18143  equivestrcsetc  18184  yoniso  18317  gsumpropd  18712  gsumpropd2lem  18713  xpsmnd  18811  xpsgrp  19101  ghmqusker  19327  gsumval3lem1  19945  gsumval3lem2  19946  gsumcom2  20015  xpsrngd  20225  xpsringd  20377  rngqiprngim  21371  coe1mul2lem2  22328  scmatrngiso  22593  m2cpmrngiso  22815  cncfcnvcn  24984  isismt  28700  usgrf1oedg  29405  wlkiswwlks2lem5  30070  clwwlkvbij  30312  eupthres  30414  eupthp1  30415  f1oeq3dd  32828  cycpmconjvlem  33318  tocyccntz  33321  idomsubr  33493  dimkerim  33921  prodeq12sdv  36575  cbvsumdavw2  36652  cbvproddavw2  36653  poimirlem4  38120  poimirlem9  38125  rngoisoval  38473  frlmsnic  43155  sge0f1o  46953  nnfoctbdj  47027  3f1oss1  47666  f1oresf1o  47881  grimidvtxedg  48504  ushggricedg  48546  uhgrimisgrgric  48550  isubgr3stgrlem3  48587  uptrlem1  49828  uptrar  49834  uptr2  49839  oduoppcciso  50184