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

Metamath Proof Explorer

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 } )