Theorem spcedv 3549

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

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

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 2115

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

This theorem is referenced by:  selsALT  5386  zfrep6  7896  ertr  8646  dom3d  8927  disjenex  9059  domssex2  9061  domssex  9062  brwdom2  9470  infxpenc2lem2  9922  dfac8clem  9934  ac5num  9938  acni2  9948  acnlem  9950  finnisoeu  10015  infpss  10118  cofsmo  10171  axdc4lem  10357  ac6num  10381  axdclem2  10422  hasheqf1od  14267  fz1isolem  14375  wrd2f1tovbij  14874  fsum  15634  ntrivcvgn0  15812  fprod  15855  setsexstruct2  17093  isacs1i  17571  mreacs  17572  gsumval3lem2  19826  eltg3  22897  elptr  23508  nbusgrf1o1  29369  cusgrexg  29443  cusgrfilem3  29457  sizusglecusg  29463  wwlksnextbij  29901  gsumhashmul  33078  fzo0pmtrlast  33102  1arithidom  33546  fineqvnttrclse  35216  gblacfnacd  35218  numiunnum  36586  bj-imdirco  37307  eqvreltr  38776  aks6d1c2  42296  sticksstones20  42332  onsucf1lem  43426  onsucf1olem  43427  nnoeomeqom  43469  rp-isfinite5  43674  clrellem  43779  clcnvlem  43780  fundcmpsurinj  47571  prproropen  47670  grimidvtxedg  48047  grimcnv  48050  grimco  48051  isuspgrim0  48056  gricushgr  48079  ushggricedg  48089  uhgrimisgrgric  48093  isgrtri  48105  usgrgrtrirex  48112  isubgr3stgrlem3  48130  isubgr3stgr  48137  uspgrlim  48154  grlimgrtri  48165  grlicref  48174  grlicsym  48175  grlictr  48177  uspgrsprfo  48310  uspgrbispr  48313  1aryenef  48807  2aryenef  48818  eufsnlem  49002  xpco2  49018  opncldeqv  49063  uobffth  49379  uobeqw  49380  thincciso  49614  thinccisod  49615  functermceu  49671  idfudiag1  49686  termcarweu  49689  arweutermc  49691  funcsn  49702  0fucterm  49704  mndtcbas  49742