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

Metamath Proof Explorer

Theorem sssn

Description: The subsets of a singleton. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion sssn ( 𝐴 ⊆ { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 neq0 ⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
2 ssel ⊢ ( 𝐴 ⊆ { 𝐵 } → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝐵 } ) )
3 elsni ⊢ ( 𝑥 ∈ { 𝐵 } → 𝑥 = 𝐵 )
4 2 3 syl6 ⊢ ( 𝐴 ⊆ { 𝐵 } → ( 𝑥 ∈ 𝐴 → 𝑥 = 𝐵 ) )
5 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
6 4 5 syl6 ⊢ ( 𝐴 ⊆ { 𝐵 } → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) ) )
7 6 ibd ⊢ ( 𝐴 ⊆ { 𝐵 } → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
8 7 exlimdv ⊢ ( 𝐴 ⊆ { 𝐵 } → ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
9 1 8 biimtrid ⊢ ( 𝐴 ⊆ { 𝐵 } → ( ¬ 𝐴 = ∅ → 𝐵 ∈ 𝐴 ) )
10 snssi ⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 )
11 9 10 syl6 ⊢ ( 𝐴 ⊆ { 𝐵 } → ( ¬ 𝐴 = ∅ → { 𝐵 } ⊆ 𝐴 ) )
12 11 anc2li ⊢ ( 𝐴 ⊆ { 𝐵 } → ( ¬ 𝐴 = ∅ → ( 𝐴 ⊆ { 𝐵 } ∧ { 𝐵 } ⊆ 𝐴 ) ) )
13 eqss ⊢ ( 𝐴 = { 𝐵 } ↔ ( 𝐴 ⊆ { 𝐵 } ∧ { 𝐵 } ⊆ 𝐴 ) )
14 12 13 imbitrrdi ⊢ ( 𝐴 ⊆ { 𝐵 } → ( ¬ 𝐴 = ∅ → 𝐴 = { 𝐵 } ) )
15 14 orrd ⊢ ( 𝐴 ⊆ { 𝐵 } → ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )
16 0ss ⊢ ∅ ⊆ { 𝐵 }
17 sseq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ⊆ { 𝐵 } ↔ ∅ ⊆ { 𝐵 } ) )
18 16 17 mpbiri ⊢ ( 𝐴 = ∅ → 𝐴 ⊆ { 𝐵 } )
19 eqimss ⊢ ( 𝐴 = { 𝐵 } → 𝐴 ⊆ { 𝐵 } )
20 18 19 jaoi ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) → 𝐴 ⊆ { 𝐵 } )
21 15 20 impbii ⊢ ( 𝐴 ⊆ { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )