Theorem spimevw 1992

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

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  dtruALT2  5300  zfpair  5351  axprlem3  5355  exneq  5376  fvn0ssdmfun  7016  axnulregtco  36717  onsupmaxb  43693  refimssco  44060  rlimdmafv  47648  rlimdmafv2  47729  elsprel  47958