Theorem f1oeq3d 6800

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 6793	. 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 1540  –1-1-onto→wf1o 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  resdif  6824  f1osng  6844  f1oresrab  7102  fveqf1o  7280  isoini2  7317  oacomf1o  8532  mapsnf1o  8915  domss2  9106  dif1enlem  9126  dif1enlemOLD  9127  infn0  9258  wemapwe  9657  oef1o  9658  cnfcomlem  9659  cnfcom3  9664  cnfcom3clem  9665  infxpenc  9978  infxpenc2lem1  9979  infxpenc2  9982  ackbij2lem2  10199  hsmexlem1  10386  fsumss  15698  fsumcnv  15746  fprodss  15921  fprodcnv  15956  pwssnf1o  17468  catcisolem  18079  equivestrcsetc  18120  yoniso  18253  gsumpropd  18612  gsumpropd2lem  18613  xpsmnd  18711  xpsgrp  18998  ghmqusker  19226  gsumval3lem1  19842  gsumval3lem2  19843  gsumcom2  19912  xpsrngd  20095  xpsringd  20248  rngqiprngim  21221  coe1mul2lem2  22161  scmatrngiso  22430  m2cpmrngiso  22652  cncfcnvcn  24826  isismt  28468  usgrf1oedg  29141  wlkiswwlks2lem5  29810  clwwlkvbij  30049  eupthres  30151  eupthp1  30152  cycpmconjvlem  33105  tocyccntz  33108  idomsubr  33266  dimkerim  33630  prodeq12sdv  36213  cbvsumdavw2  36290  cbvproddavw2  36291  poimirlem4  37625  poimirlem9  37630  rngoisoval  37978  frlmsnic  42535  sge0f1o  46387  nnfoctbdj  46461  3f1oss1  47080  f1oresf1o  47295  grimidvtxedg  47889  ushggricedg  47931  uhgrimisgrgric  47935  isubgr3stgrlem3  47971  uptrlem1  49203  uptrar  49209  uptr2  49214  oduoppcciso  49559