Metamath Proof Explorer

Theorem sspr

Description: The subsets of a pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion sspr ⊢A⊆BC↔A=∅∨A=B∨A=C∨A=BC

Proof

Step Hyp Ref Expression
1 uncom ⊢∅∪BC=BC∪∅
2 un0 ⊢BC∪∅=BC
3 1 2 eqtri ⊢∅∪BC=BC
4 3 sseq2i ⊢A⊆∅∪BC↔A⊆BC
5 0ss ⊢∅⊆A
6 5 biantrur ⊢A⊆∅∪BC↔∅⊆A∧A⊆∅∪BC
7 4 6 bitr3i ⊢A⊆BC↔∅⊆A∧A⊆∅∪BC
8 ssunpr ⊢∅⊆A∧A⊆∅∪BC↔A=∅∨A=∅∪B∨A=∅∪C∨A=∅∪BC
9 uncom ⊢∅∪B=B∪∅
10 un0 ⊢B∪∅=B
11 9 10 eqtri ⊢∅∪B=B
12 11 eqeq2i ⊢A=∅∪B↔A=B
13 12 orbi2i ⊢A=∅∨A=∅∪B↔A=∅∨A=B
14 uncom ⊢∅∪C=C∪∅
15 un0 ⊢C∪∅=C
16 14 15 eqtri ⊢∅∪C=C
17 16 eqeq2i ⊢A=∅∪C↔A=C
18 3 eqeq2i ⊢A=∅∪BC↔A=BC
19 17 18 orbi12i ⊢A=∅∪C∨A=∅∪BC↔A=C∨A=BC
20 13 19 orbi12i ⊢A=∅∨A=∅∪B∨A=∅∪C∨A=∅∪BC↔A=∅∨A=B∨A=C∨A=BC
21 7 8 20 3bitri ⊢A⊆BC↔A=∅∨A=B∨A=C∨A=BC