Theorem f1oeq3d 6844

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 6837	. 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 1539  –1-1-onto→wf1o 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ss 3967  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567

This theorem is referenced by:  resdif  6868  f1osng  6888  f1oresrab  7146  fveqf1o  7323  isoini2  7360  oacomf1o  8604  mapsnf1o  8980  domss2  9177  dif1enlem  9197  dif1enlemOLD  9198  infn0  9341  wemapwe  9738  oef1o  9739  cnfcomlem  9740  cnfcom3  9745  cnfcom3clem  9746  infxpenc  10059  infxpenc2lem1  10060  infxpenc2  10063  ackbij2lem2  10280  hsmexlem1  10467  fsumss  15762  fsumcnv  15810  fprodss  15985  fprodcnv  16020  pwssnf1o  17544  catcisolem  18156  equivestrcsetc  18198  yoniso  18331  gsumpropd  18692  gsumpropd2lem  18693  xpsmnd  18791  xpsgrp  19078  ghmqusker  19306  gsumval3lem1  19924  gsumval3lem2  19925  gsumcom2  19994  xpsrngd  20177  xpsringd  20330  rngqiprngim  21315  coe1mul2lem2  22272  scmatrngiso  22543  m2cpmrngiso  22765  cncfcnvcn  24953  isismt  28543  usgrf1oedg  29225  wlkiswwlks2lem5  29894  clwwlkvbij  30133  eupthres  30235  eupthp1  30236  cycpmconjvlem  33162  tocyccntz  33165  idomsubr  33312  dimkerim  33679  prodeq12sdv  36220  cbvsumdavw2  36297  cbvproddavw2  36298  poimirlem4  37632  poimirlem9  37637  rngoisoval  37985  frlmsnic  42555  sge0f1o  46402  nnfoctbdj  46476  3f1oss1  47092  f1oresf1o  47307  grimidvtxedg  47881  ushggricedg  47901  uhgrimisgrgric  47904  isubgr3stgrlem3  47940  oduoppcciso  49218