Metamath Proof Explorer

Theorem leftssold

Description: The left options are a subset of the old set. (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Assertion leftssold 
|- ( _Left ` X ) C_ ( _Old ` ( bday ` X ) )

Proof

Step Hyp Ref Expression
1 leftval 
 |-  ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
2 ssrab2 
 |-  { x e. ( _Old ` ( bday ` X ) ) | x
3 1 2 eqsstri 
 |-  ( _Left ` X ) C_ ( _Old ` ( bday ` X ) )