Metamath Proof Explorer

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 φ y z φ


Step Hyp Ref Expression
1 ax-frege52c x = y [˙x / z]˙ φ [˙y / z]˙ φ
2 sbsbc x z φ [˙x / z]˙ φ
3 sbsbc y z φ [˙y / z]˙ φ
4 1 2 3 3imtr4g x = y x z φ y z φ