Theorem dmsnopg

Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	dmsnopg	|- ( B e. V -> dom { <. A , B >. } = { A } )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		vex	|- y e. _V
3	1 2	opth1	|- ( <. x , y >. = <. A , B >. -> x = A )
4	3	exlimiv	|- ( E. y <. x , y >. = <. A , B >. -> x = A )
5		opeq1	|- ( x = A -> <. x , B >. = <. A , B >. )
6		opeq2	|- ( y = B -> <. x , y >. = <. x , B >. )
7	6	eqeq1d	|- ( y = B -> ( <. x , y >. = <. A , B >. <-> <. x , B >. = <. A , B >. ) )
8	7	spcegv	|- ( B e. V -> ( <. x , B >. = <. A , B >. -> E. y <. x , y >. = <. A , B >. ) )
9	5 8	syl5	|- ( B e. V -> ( x = A -> E. y <. x , y >. = <. A , B >. ) )
10	4 9	impbid2	|- ( B e. V -> ( E. y <. x , y >. = <. A , B >. <-> x = A ) )
11	1	eldm2	|- ( x e. dom { <. A , B >. } <-> E. y <. x , y >. e. { <. A , B >. } )
12		opex	|- <. x , y >. e. _V
13	12	elsn	|- ( <. x , y >. e. { <. A , B >. } <-> <. x , y >. = <. A , B >. )
14	13	exbii	|- ( E. y <. x , y >. e. { <. A , B >. } <-> E. y <. x , y >. = <. A , B >. )
15	11 14	bitri	|- ( x e. dom { <. A , B >. } <-> E. y <. x , y >. = <. A , B >. )
16		velsn	|- ( x e. { A } <-> x = A )
17	10 15 16	3bitr4g	|- ( B e. V -> ( x e. dom { <. A , B >. } <-> x e. { A } ) )
18	17	eqrdv	|- ( B e. V -> dom { <. A , B >. } = { A } )