Metamath Proof Explorer

Theorem frege55lem2b

Description: Lemma for frege55b . Core proof of Proposition 55 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege55lem2b 
|- ( x = y -> [ y / z ] z = x )

Proof

Step Hyp Ref Expression
1 frege54cor1b 
 |-  [ x / z ] z = x
2 frege53b 
 |-  ( [ x / z ] z = x -> ( x = y -> [ y / z ] z = x ) )
3 1 2 ax-mp 
 |-  ( x = y -> [ y / z ] z = x )