Theorem spimevw 2001

Description: Existential introduction, using implicit substitution. This is to spimew 1974 what spimvw 2002 is to spimw 1973. Version of spimev 2399 and spimefv 2196 with an additional disjoint variable condition, using only Tarski's FOL axiom schemes. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 17-Mar-2020.)

Hypothesis

Ref	Expression
spimevw.1	⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))

Assertion

Ref	Expression
spimevw	⊢ (𝜑 → ∃𝑥𝜓)

Distinct variable groups:   𝑥,𝑦   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem spimevw

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1974	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1781

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 1911  ax-6 1970

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  zfpair  5287  fvn0ssdmfun  6819  bj-dtru  34254  sn-dtru  39403  refimssco  40307  rlimdmafv  43733  rlimdmafv2  43814  elsprel  43992