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

Metamath Proof Explorer

Theorem dmsnopss

Description: The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B ). (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion dmsnopss 
|- dom { <. A , B >. } C_ { A }

Proof

Step Hyp Ref Expression
1 dmsnopg 
 |-  ( B e. _V -> dom { <. A , B >. } = { A } )
2 eqimss 
 |-  ( dom { <. A , B >. } = { A } -> dom { <. A , B >. } C_ { A } )
3 1 2 syl 
 |-  ( B e. _V -> dom { <. A , B >. } C_ { A } )
4 opprc2 
 |-  ( -. B e. _V -> <. A , B >. = (/) )
5 4 sneqd 
 |-  ( -. B e. _V -> { <. A , B >. } = { (/) } )
6 5 dmeqd 
 |-  ( -. B e. _V -> dom { <. A , B >. } = dom { (/) } )
7 dmsn0 
 |-  dom { (/) } = (/)
8 6 7 eqtrdi 
 |-  ( -. B e. _V -> dom { <. A , B >. } = (/) )
9 0ss 
 |-  (/) C_ { A }
10 8 9 eqsstrdi 
 |-  ( -. B e. _V -> dom { <. A , B >. } C_ { A } )
11 3 10 pm2.61i 
 |-  dom { <. A , B >. } C_ { A }