Metamath Proof Explorer

Theorem rere

Description: A real number equals its real part. One direction of Proposition 10-3.4(f) of Gleason p. 133. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Assertion rere A A = A


Step Hyp Ref Expression
1 recn A A
2 rereb A A A = A
3 1 2 syl A A A = A
4 3 ibi A A = A