Metamath Proof Explorer

Theorem rightssold

Description: The right options are a subset of the old set. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion rightssold 
|- ( X e. No -> ( _R ` X ) C_ ( _Old ` ( bday ` X ) ) )

Proof

Step Hyp Ref Expression
1 rightval 
 |-  ( X e. No -> ( _R ` X ) = { x e. ( _Old ` ( bday ` X ) ) | X
2 ssrab2 
 |-  { x e. ( _Old ` ( bday ` X ) ) | X
3 1 2 eqsstrdi 
 |-  ( X e. No -> ( _R ` X ) C_ ( _Old ` ( bday ` X ) ) )