Theorem spimevw 2012

Description: Existential introduction, using implicit substitution. This is to spimew 1998 what spimvw 2013 is to spimw 1997. Version of spimev 2430 and spimefv 2240 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 1937	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1998	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994

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

This theorem is referenced by:  dtruALT2  5342  zfpair  5393  axprlem3  5397  exneq  5418  fvn0ssdmfun  7070  axnulregtco  36914  onsupmaxb  43892  refimssco  44259  rlimdmafv  47837  rlimdmafv2  47918  elsprel  48147