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

Metamath Proof Explorer

Theorem stdpc7

Description: One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 .) Translated to traditional notation, it can be read: " x = y -> ( ph ( x , x ) -> ph ( x , y ) ) , provided that y is free for x in ph ( x , x ) ". Axiom 7 of Mendelson p. 95. (Contributed by NM, 15-Feb-2005)

		Ref	Expression
	Assertion	stdpc7	\|- ( x = y -> ( [ x / y ] ph -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ2	\|- ( y = x -> ( [ x / y ] ph -> ph ) )
2	1	equcoms	\|- ( x = y -> ( [ x / y ] ph -> ph ) )