Theorem spimevw 1994

Description: Existential introduction, using implicit substitution. This is to spimew 1971 what spimvw 1995 is to spimw 1970. Version of spimev 2400 and spimefv 2199 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 1909	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1971	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  dtruALT2  5388  zfpair  5439  exneq  5455  dtruOLD  5461  fvn0ssdmfun  7108  onsupmaxb  43200  refimssco  43569  rlimdmafv  47092  rlimdmafv2  47173  elsprel  47349