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 -> ( [ x / z ] ph -> [ y / z ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax-frege52c	|- ( x = y -> ( [. x / z ]. ph -> [. y / z ]. ph ) )
2		sbsbc	|- ( [ x / z ] ph <-> [. x / z ]. ph )
3		sbsbc	|- ( [ y / z ] ph <-> [. y / z ]. ph )
4	1 2 3	3imtr4g	|- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )