Theorem spw

Description: Weak version of the specialization scheme sp . Lemma 9 of KalishMontague p. 87. While it appears that sp in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove anyinstance of sp having mutually distinct setvar variables and no wff metavariables (see ax12wdemo for an example of the procedure to eliminate the hypothesis). Other approximations of sp are spfw (minimal distinct variable requirements), spnfw (when x is not free in -. ph ), spvw (when x does not appear in ph ), sptruw (when ph is true), spfalw (when ph is false), and spvv (where ph is changed into ps ). (Contributed by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 27-Feb-2018)

	Ref	Expression
Hypothesis	spw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	spw	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		spw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		ax-5	⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 )
3		ax-5	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
4		ax-5	⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 )
5	2 3 4 1	spfw	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )