Theorem dmsnopg 5200

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

Assertion

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

Proof of Theorem dmsnopg

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2802	. . . . . 6 |- x e. _V
2		vex 2802	. . . . . 6 |- y e. _V
3	1, 2	opth1 4322	. . . . 5 |- ( <. x , y >. = <. A , B >. -> x = A )
4	3	exlimiv 1644	. . . 4 |- ( E. y <. x , y >. = <. A , B >. -> x = A )
5		opeq1 3857	. . . . 5 |- ( x = A -> <. x , B >. = <. A , B >. )
6		opeq2 3858	. . . . . . 7 |- ( y = B -> <. x , y >. = <. x , B >. )
7	6	eqeq1d 2238	. . . . . 6 |- ( y = B -> ( <. x , y >. = <. A , B >. <-> <. x , B >. = <. A , B >. ) )
8	7	spcegv 2891	. . . . 5 |- ( B e. V -> ( <. x , B >. = <. A , B >. -> E. y <. x , y >. = <. A , B >. ) )
9	5, 8	syl5 32	. . . 4 |- ( B e. V -> ( x = A -> E. y <. x , y >. = <. A , B >. ) )
10	4, 9	impbid2 143	. . 3 |- ( B e. V -> ( E. y <. x , y >. = <. A , B >. <-> x = A ) )
11	1	eldm2 4921	. . . 4 |- ( x e. dom { <. A , B >. } <-> E. y <. x , y >. e. { <. A , B >. } )
12	1, 2	opex 4315	. . . . . 6 |- <. x , y >. e. _V
13	12	elsn 3682	. . . . 5 |- ( <. x , y >. e. { <. A , B >. } <-> <. x , y >. = <. A , B >. )
14	13	exbii 1651	. . . 4 |- ( E. y <. x , y >. e. { <. A , B >. } <-> E. y <. x , y >. = <. A , B >. )
15	11, 14	bitri 184	. . 3 |- ( x e. dom { <. A , B >. } <-> E. y <. x , y >. = <. A , B >. )
16		velsn 3683	. . 3 |- ( x e. { A } <-> x = A )
17	10, 15, 16	3bitr4g 223	. 2 |- ( B e. V -> ( x e. dom { <. A , B >. } <-> x e. { A } ) )
18	17	eqrdv 2227	1 |- ( B e. V -> dom { <. A , B >. } = { A } )

Syntax hints:   -> wi 4   = wceq 1395   E.wex 1538   e. wcel 2200   {csn 3666   <.cop 3669   dom cdm 4719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-dm 4729

This theorem is referenced by:  dmpropg  5201  dmsnop  5202  rnsnopg  5207  elxp4  5216  fnsng  5368  funprg  5371  funtpg  5372  fntpg  5377  s1dmg  11158  ennnfonelemhdmp1  12980  ennnfonelemkh  12983  setsvala  13063  setsresg  13070  setscom  13072  setsslid  13083  bassetsnn  13089  strle1g  13139