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 ( 𝑥 = 𝐴[ 𝐴 / 𝑧 ] 𝑧 = 𝑥 )

Proof

Step Hyp Ref Expression
1 vex 𝑥 ∈ V
2 1 frege54cor1c [ 𝑥 / 𝑧 ] 𝑧 = 𝑥
3 frege53c ( [ 𝑥 / 𝑧 ] 𝑧 = 𝑥 → ( 𝑥 = 𝐴[ 𝐴 / 𝑧 ] 𝑧 = 𝑥 ) )
4 2 3 ax-mp ( 𝑥 = 𝐴[ 𝐴 / 𝑧 ] 𝑧 = 𝑥 )