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 L X Old bday X

Proof

Step Hyp Ref Expression
1 leftval L X = x Old bday X | x < s X
2 ssrab2 x Old bday X | x < s X Old bday X
3 1 2 eqsstri L X Old bday X