Theorem spcev 2946

Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypotheses

Ref	Expression
spcv.1	⊢ A ∈ V
spcv.2	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
spcev	⊢ (ψ → ∃xφ)

Distinct variable groups:   x,A   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem spcev

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ A ∈ V
2		spcv.2	. . 3 ⊢ (x = A → (φ ↔ ψ))
3	2	spcegv 2940	. 2 ⊢ (A ∈ V → (ψ → ∃xφ))
4	1, 3	ax-mp 8	1 ⊢ (ψ → ∃xφ)

Syntax hints:   → wi 4   ↔ wb 176  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861

This theorem is referenced by:  snel1c  4140  sspw1  4335  sspw12  4336  sfin01  4528  sfindbl  4530  1cvsfin  4542  vfinspsslem1  4550  phialllem1  4616  phialllem2  4617  nfunv  5138  ffoss  5314  map0  6025  unen  6048  enpw1  6062  1cnc  6139  ncaddccl  6144  ce0addcnnul  6179  ce0nulnc  6184  dflec3  6221  nclenc  6222