Metamath Proof Explorer


Theorem frege54cor1b

Description: Reflexive equality. (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion frege54cor1b [ 𝑥 / 𝑦 ] 𝑦 = 𝑥

Proof

Step Hyp Ref Expression
1 equsb1 [ 𝑥 / 𝑦 ] 𝑦 = 𝑥