Metamath Proof Explorer

Theorem elright

Description: Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion elright 
|- ( A e. ( _Right ` B ) <-> ( A e. ( _Old ` ( bday ` B ) ) /\ B

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = A -> ( B  B
2 rightval 
 |-  ( _Right ` B ) = { x e. ( _Old ` ( bday ` B ) ) | B
3 1 2 elrab2 
 |-  ( A e. ( _Right ` B ) <-> ( A e. ( _Old ` ( bday ` B ) ) /\ B