Theorem spimevw 1992

Description: Existential introduction, using implicit substitution. This is to spimew 1969 what spimvw 1993 is to spimw 1968. Version of spimev 2395 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 1908	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1969	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965

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

This theorem is referenced by:  dtruALT2  5376  zfpair  5427  axprlem3  5431  exneq  5446  dtruOLD  5452  fvn0ssdmfun  7094  onsupmaxb  43228  refimssco  43597  rlimdmafv  47127  rlimdmafv2  47208  elsprel  47400