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

Metamath Proof Explorer

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 
|- ( x = y -> ( ph <-> ps ) )
Assertion spw 
|- ( A. x ph -> ph )

Proof

Step Hyp Ref Expression
1 spw.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 ax-5 
 |-  ( -. ps -> A. x -. ps )
3 ax-5 
 |-  ( A. x ph -> A. y A. x ph )
4 ax-5 
 |-  ( -. ph -> A. y -. ph )
5 2 3 4 1 spfw 
 |-  ( A. x ph -> ph )