Metamath Proof Explorer


Theorem disjpss

Description: A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004)

Ref Expression
Assertion disjpss A B = B A A B

Proof

Step Hyp Ref Expression
1 ssid B B
2 1 biantru B A B A B B
3 ssin B A B B B A B
4 2 3 bitri B A B A B
5 sseq2 A B = B A B B
6 4 5 syl5bb A B = B A B
7 ss0 B B =
8 6 7 syl6bi A B = B A B =
9 8 necon3ad A B = B ¬ B A
10 9 imp A B = B ¬ B A
11 nsspssun ¬ B A A B A
12 uncom B A = A B
13 12 psseq2i A B A A A B
14 11 13 bitri ¬ B A A A B
15 10 14 sylib A B = B A A B