Metamath Proof Explorer

Theorem frege55lem2c

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

Ref Expression
Assertion frege55lem2c 
|- ( x = A -> [. A / z ]. z = x )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 frege54cor1c 
 |-  [. x / z ]. z = x
3 frege53c 
 |-  ( [. x / z ]. z = x -> ( x = A -> [. A / z ]. z = x ) )
4 2 3 ax-mp 
 |-  ( x = A -> [. A / z ]. z = x )