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 }