Theorem frege52b

Description: The case when the content of x is identical with the content of y and in which a proposition controlled by an element for which we substitute the content of x is affirmed and the same proposition, this time where we substitute the content of y , is denied does not take place. In [ x / z ] ph , x can also occur in other than the argument ( z ) places. Hence x may still be contained in [ y / z ] ph . Part of Axiom 52 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege52b	$$⊢x=y\to \left(\left[x/z\right]\phi \to \left[y/z\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-frege52c	$$⊢x=y\to \left(\underset{\dot{}}{[}x/z\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}y/z\underset{\dot{}}{]}\phi \right)$$
2		sbsbc	$$⊢\left[x/z\right]\phi \leftrightarrow \underset{\dot{}}{[}x/z\underset{\dot{}}{]}\phi$$
3		sbsbc	$$⊢\left[y/z\right]\phi \leftrightarrow \underset{\dot{}}{[}y/z\underset{\dot{}}{]}\phi$$
4	1 2 3	3imtr4g	$$⊢x=y\to \left(\left[x/z\right]\phi \to \left[y/z\right]\phi \right)$$