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	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ2	⊢ ( 𝑦 = 𝑥 → ( [ 𝑥 / 𝑦 ] 𝜑 → 𝜑 ) )
2	1	equcoms	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 → 𝜑 ) )