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\to \left(\left[x/y\right]\phi \to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbequ2	$$⊢y=x\to \left(\left[x/y\right]\phi \to \phi \right)$$
2	1	equcoms	$$⊢x=y\to \left(\left[x/y\right]\phi \to \phi \right)$$