Theorem spimew 1975

Description: Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Wolf Lammen, 22-Oct-2023.)

Hypotheses

Ref	Expression
spimew.1	⊢ (𝜑 → ∀𝑥𝜑)
spimew.2	⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))

Assertion

Ref	Expression
spimew	⊢ (𝜑 → ∃𝑥𝜓)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem spimew

Step	Hyp	Ref	Expression
1		ax6v 1972	. 2 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
2		spimew.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		spimew.2	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	3	speimfw 1967	. 2 ⊢ (¬ ∀𝑥 ¬ 𝑥 = 𝑦 → (∀𝑥𝜑 → ∃𝑥𝜓))
5	1, 2, 4	mpsyl 68	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  speiv  1976  spimevw  1998  bj-cbvexiw  34852