Theorem spimevw 1999

Description: Existential introduction, using implicit substitution. This is to spimew 1976 what spimvw 2000 is to spimw 1975. Version of spimev 2392 and spimefv 2192 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 1914	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1976	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  dtruALT2  5369  zfpair  5420  exneq  5436  dtruOLD  5442  fvn0ssdmfun  7077  onsupmaxb  41988  refimssco  42358  rlimdmafv  45885  rlimdmafv2  45966  elsprel  46143