Metamath Proof Explorer

Theorem frege54cor1b

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

Ref Expression
Assertion frege54cor1b 
|- [ x / y ] y = x

Proof

Step Hyp Ref Expression
1 equsb1 
 |-  [ x / y ] y = x