Metamath Proof Explorer


Theorem left0s

Description: The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion left0s L0s=

Proof

Step Hyp Ref Expression
1 leftssold L0sOldbday0s
2 bday0s bday0s=
3 2 fveq2i Oldbday0s=Old
4 old0 Old=
5 3 4 eqtri Oldbday0s=
6 sseq0 L0sOldbday0sOldbday0s=L0s=
7 1 5 6 mp2an L0s=