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 }