This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊆ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C

Proof

Step Hyp Ref Expression
1 0un ⊢ ∅ ∪ B C = B C
2 1 sseq2i ⊢ A ⊆ ∅ ∪ B C ↔ A ⊆ B C
3 0ss ⊢ ∅ ⊆ A
4 3 biantrur ⊢ A ⊆ ∅ ∪ B C ↔ ∅ ⊆ A ∧ A ⊆ ∅ ∪ B C
5 2 4 bitr3i ⊢ A ⊆ B C ↔ ∅ ⊆ A ∧ A ⊆ ∅ ∪ B C
6 ssunpr ⊢ ∅ ⊆ A ∧ A ⊆ ∅ ∪ B C ↔ A = ∅ ∨ A = ∅ ∪ B ∨ A = ∅ ∪ C ∨ A = ∅ ∪ B C
7 0un ⊢ ∅ ∪ B = B
8 7 eqeq2i ⊢ A = ∅ ∪ B ↔ A = B
9 8 orbi2i ⊢ A = ∅ ∨ A = ∅ ∪ B ↔ A = ∅ ∨ A = B
10 0un ⊢ ∅ ∪ C = C
11 10 eqeq2i ⊢ A = ∅ ∪ C ↔ A = C
12 1 eqeq2i ⊢ A = ∅ ∪ B C ↔ A = B C
13 11 12 orbi12i ⊢ A = ∅ ∪ C ∨ A = ∅ ∪ B C ↔ A = C ∨ A = B C
14 9 13 orbi12i ⊢ A = ∅ ∨ A = ∅ ∪ B ∨ A = ∅ ∪ C ∨ A = ∅ ∪ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C
15 5 6 14 3bitri ⊢ A ⊆ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C