This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spim

Description: Specialization, using implicit substitution. Compare Lemma 14 of Tarski p. 70. The spim series of theorems requires that only one direction of the substitution hypothesis hold. Usage of this theorem is discouraged because it depends on ax-13 . See spimw for a version requiring fewer axioms. (Contributed by NM, 10-Jan-1993) (Revised by Mario Carneiro, 3-Oct-2016) (Proof shortened by Wolf Lammen, 18-Feb-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spim.1	⊢ Ⅎ 𝑥 𝜓
	spim.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
Assertion	spim	⊢ ( ∀ 𝑥 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		spim.1	⊢ Ⅎ 𝑥 𝜓
2		spim.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
3		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦
4	3 2	eximii	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
5	1 4	19.36i	⊢ ( ∀ 𝑥 𝜑 → 𝜓 )