Metamath Proof Explorer


Theorem left0s

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

Ref Expression
Assertion left0s L 0 s =

Proof

Step Hyp Ref Expression
1 leftssold L 0 s Old bday 0 s
2 bday0s bday 0 s =
3 2 fveq2i Old bday 0 s = Old
4 old0 Old =
5 3 4 eqtri Old bday 0 s =
6 sseq0 L 0 s Old bday 0 s Old bday 0 s = L 0 s =
7 1 5 6 mp2an L 0 s =