Theorem spcedv 3558

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 3557	. 2 ⊢ (𝑋 ∈ 𝑉 → (𝜒 → ∃𝑥𝜓))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∃wex 1781   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-clel 2809

This theorem is referenced by:  selsALT  5401  zfrep6  7892  wfrlem15OLD  8274  ertr  8670  f1dom2gOLD  8917  dom3d  8941  disjenex  9086  domssex2  9088  domssex  9089  brwdom2  9518  infxpenc2lem2  9965  dfac8clem  9977  ac5num  9981  acni2  9991  acnlem  9993  finnisoeu  10058  infpss  10162  cofsmo  10214  axdc4lem  10400  ac6num  10424  axdclem2  10465  hasheqf1od  14263  fz1isolem  14372  wrd2f1tovbij  14861  fsum  15616  ntrivcvgn0  15794  fprod  15835  setsexstruct2  17058  isacs1i  17551  mreacs  17552  gsumval3lem2  19697  eltg3  22349  elptr  22961  nbusgrf1o1  28381  cusgrexg  28455  cusgrfilem3  28468  sizusglecusg  28474  wwlksnextbij  28910  gsumhashmul  31968  bj-imdirco  35734  eqvreltr  37142  sticksstones20  40647  onsucf1lem  41662  onsucf1olem  41663  nnoeomeqom  41705  rp-isfinite5  41911  clrellem  42016  clcnvlem  42017  fundcmpsurinj  45721  prproropen  45820  isomgreqve  46137  isomushgr  46138  isomgrsym  46148  isomgrtr  46151  ushrisomgr  46153  uspgrsprfo  46170  uspgrbispr  46173  1aryenef  46851  2aryenef  46862  eufsnlem  47027  opncldeqv  47054  thincciso  47189  mndtcbas  47227