Theorem spimevw 2006

Description: Existential introduction, using implicit substitution. This is to spimew 1992 what spimvw 2007 is to spimw 1991. Version of spimev 2424 and spimefv 2234 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 1931	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		spimevw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	1, 2	spimew 1992	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988

This theorem depends on definitions:  df-bi 209  df-ex 1801

This theorem is referenced by:  dtruALT2  5328  zfpair  5379  axprlem3  5383  exneq  5404  fvn0ssdmfun  7056  axnulregtco  36841  onsupmaxb  43817  refimssco  44184  rlimdmafv  47772  rlimdmafv2  47853  elsprel  48082