Metamath Proof Explorer

Theorem elleft

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

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

Proof

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