Theorem spcedv 3577

Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.)

Hypotheses

Ref	Expression
spcedv.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)
spcedv.2	⊢ (𝜑 → 𝜒)
spcedv.3	⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
spcedv	⊢ (𝜑 → ∃𝑥𝜓)

Distinct variable groups:   𝑥,𝑋   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem spcedv

Step	Hyp	Ref	Expression
1		spcedv.1	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
2		spcedv.2	. 2 ⊢ (𝜑 → 𝜒)
3		spcedv.3	. . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))
4	3	spcegv 3576	. 2 ⊢ (𝑋 ∈ 𝑉 → (𝜒 → ∃𝑥𝜓))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108

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 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-clel 2809

This theorem is referenced by:  selsALT  5414  zfrep6  7953  wfrlem15OLD  8337  ertr  8734  dom3d  9008  disjenex  9149  domssex2  9151  domssex  9152  brwdom2  9587  infxpenc2lem2  10034  dfac8clem  10046  ac5num  10050  acni2  10060  acnlem  10062  finnisoeu  10127  infpss  10230  cofsmo  10283  axdc4lem  10469  ac6num  10493  axdclem2  10534  hasheqf1od  14371  fz1isolem  14479  wrd2f1tovbij  14979  fsum  15736  ntrivcvgn0  15914  fprod  15957  setsexstruct2  17194  isacs1i  17669  mreacs  17670  gsumval3lem2  19887  eltg3  22900  elptr  23511  nbusgrf1o1  29349  cusgrexg  29423  cusgrfilem3  29437  sizusglecusg  29443  wwlksnextbij  29884  gsumhashmul  33055  fzo0pmtrlast  33103  1arithidom  33552  gblacfnacd  35130  numiunnum  36488  bj-imdirco  37208  eqvreltr  38625  aks6d1c2  42143  sticksstones20  42179  onsucf1lem  43293  onsucf1olem  43294  nnoeomeqom  43336  rp-isfinite5  43541  clrellem  43646  clcnvlem  43647  fundcmpsurinj  47423  prproropen  47522  grimidvtxedg  47898  grimcnv  47901  grimco  47902  isuspgrim0  47907  gricushgr  47930  ushggricedg  47940  uhgrimisgrgric  47944  isgrtri  47955  usgrgrtrirex  47962  isubgr3stgrlem3  47980  isubgr3stgr  47987  uspgrlim  48004  grlimgrtri  48008  grlicref  48017  grlicsym  48018  grlictr  48020  uspgrsprfo  48123  uspgrbispr  48126  1aryenef  48625  2aryenef  48636  eufsnlem  48819  opncldeqv  48876  thincciso  49339  thinccisod  49340  functermceu  49395  idfudiag1  49410  termcarweu  49413  arweutermc  49415  mndtcbas  49458