Theorem f1oeq3d 6814

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 6807	. 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 6532

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 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  resdif  6839  f1osng  6860  f1oresrab  7121  fveqf1o  7303  isoini2  7340  oacomf1o  8552  mapsnf1o  8946  domss2  9134  dif1enlem  9154  infn0  9272  wemapwe  9676  oef1o  9677  cnfcomlem  9678  cnfcom3  9683  cnfcom3clem  9684  infxpenc  10021  infxpenc2lem1  10022  infxpenc2  10025  ackbij2lem2  10241  hsmexlem1  10428  fsumss  15811  fsumcnv  15859  fprodss  16035  fprodcnv  16070  pwssnf1o  17584  catcisolem  18199  equivestrcsetc  18240  yoniso  18373  gsumpropd  18780  gsumpropd2lem  18781  xpsmnd  18884  xpsgrp  19182  ghmqusker  19414  gsumval3lem1  20032  gsumval3lem2  20033  gsumcom2  20102  xpsrngd  20314  xpsringd  20473  rngqiprngim  21507  coe1mul2lem2  22494  scmatrngiso  22758  m2cpmrngiso  22983  cncfcnvcn  25153  isismt  28876  usgrf1oedg  29667  wlkiswwlks2lem5  30341  clwwlkvbij  30583  eupthres  30695  eupthp1  30696  f1oeq3dd  33102  cycpmconjvlem  33581  tocyccntz  33584  idomsubr  33750  dimkerim  34137  prodeq12sdv  36838  cbvsumdavw2  36915  cbvproddavw2  36916  poimirlem4  38373  poimirlem9  38378  rngoisoval  38727  frlmsnic  43422  sge0f1o  47210  nnfoctbdj  47284  3f1oss1  47963  f1oresf1o  48178  grimidvtxedg  48801  ushggricedg  48843  uhgrimisgrgric  48847  isubgr3stgrlem3  48884  uptrlem1  50136  uptrar  50142  uptr2  50147  oduoppcciso  50492