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

Metamath Proof Explorer

Theorem difprsnss

Description: Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion difprsnss ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ⊆ { 𝐵 }

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 elpr ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
3 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
4 3 notbii ⊢ ( ¬ 𝑥 ∈ { 𝐴 } ↔ ¬ 𝑥 = 𝐴 )
5 biorf ⊢ ( ¬ 𝑥 = 𝐴 → ( 𝑥 = 𝐵 ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
6 5 biimparc ⊢ ( ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 = 𝐵 )
7 2 4 6 syl2anb ⊢ ( ( 𝑥 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑥 ∈ { 𝐴 } ) → 𝑥 = 𝐵 )
8 eldif ⊢ ( 𝑥 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑥 ∈ { 𝐴 } ) )
9 velsn ⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
10 7 8 9 3imtr4i ⊢ ( 𝑥 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) → 𝑥 ∈ { 𝐵 } )
11 10 ssriv ⊢ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ⊆ { 𝐵 }