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 
|- ( { A , B } \ { A } ) C_ { B }

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 elpr 
 |-  ( x e. { A , B } <-> ( x = A \/ x = B ) )
3 velsn 
 |-  ( x e. { A } <-> x = A )
4 3 notbii 
 |-  ( -. x e. { A } <-> -. x = A )
5 biorf 
 |-  ( -. x = A -> ( x = B <-> ( x = A \/ x = B ) ) )
6 5 biimparc 
 |-  ( ( ( x = A \/ x = B ) /\ -. x = A ) -> x = B )
7 2 4 6 syl2anb 
 |-  ( ( x e. { A , B } /\ -. x e. { A } ) -> x = B )
8 eldif 
 |-  ( x e. ( { A , B } \ { A } ) <-> ( x e. { A , B } /\ -. x e. { A } ) )
9 velsn 
 |-  ( x e. { B } <-> x = B )
10 7 8 9 3imtr4i 
 |-  ( x e. ( { A , B } \ { A } ) -> x e. { B } )
11 10 ssriv 
 |-  ( { A , B } \ { A } ) C_ { B }