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 ) )