Theorem spcedv 3548

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  selsALT  5377  zfrep6  7882  ertr  8632  dom3d  8911  disjenex  9043  domssex2  9045  domssex  9046  brwdom2  9454  infxpenc2lem2  9906  dfac8clem  9918  ac5num  9922  acni2  9932  acnlem  9934  finnisoeu  9999  infpss  10102  cofsmo  10155  axdc4lem  10341  ac6num  10365  axdclem2  10406  hasheqf1od  14255  fz1isolem  14363  wrd2f1tovbij  14862  fsum  15622  ntrivcvgn0  15800  fprod  15843  setsexstruct2  17081  isacs1i  17558  mreacs  17559  gsumval3lem2  19813  eltg3  22872  elptr  23483  nbusgrf1o1  29343  cusgrexg  29417  cusgrfilem3  29431  sizusglecusg  29437  wwlksnextbij  29875  gsumhashmul  33033  fzo0pmtrlast  33053  1arithidom  33494  fineqvnttrclse  35136  gblacfnacd  35138  numiunnum  36504  bj-imdirco  37224  eqvreltr  38644  aks6d1c2  42163  sticksstones20  42199  onsucf1lem  43302  onsucf1olem  43303  nnoeomeqom  43345  rp-isfinite5  43550  clrellem  43655  clcnvlem  43656  fundcmpsurinj  47440  prproropen  47539  grimidvtxedg  47916  grimcnv  47919  grimco  47920  isuspgrim0  47925  gricushgr  47948  ushggricedg  47958  uhgrimisgrgric  47962  isgrtri  47974  usgrgrtrirex  47981  isubgr3stgrlem3  47999  isubgr3stgr  48006  uspgrlim  48023  grlimgrtri  48034  grlicref  48043  grlicsym  48044  grlictr  48046  uspgrsprfo  48179  uspgrbispr  48182  1aryenef  48677  2aryenef  48688  eufsnlem  48872  xpco2  48888  opncldeqv  48933  uobffth  49250  uobeqw  49251  thincciso  49485  thinccisod  49486  functermceu  49542  idfudiag1  49557  termcarweu  49560  arweutermc  49562  funcsn  49573  0fucterm  49575  mndtcbas  49613