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 ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ⊆ { 𝐵 }