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

Proof

Step	Hyp	Ref	Expression
1		ax-frege52c	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑧 ] 𝜑 → [ 𝑦 / 𝑧 ] 𝜑 ) )
2		sbsbc	⊢ ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] 𝜑 )
3		sbsbc	⊢ ( [ 𝑦 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑧 ] 𝜑 )
4	1 2 3	3imtr4g	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑧 ] 𝜑 → [ 𝑦 / 𝑧 ] 𝜑 ) )