MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmsnopg Structured version   Visualization version   Unicode version

Theorem dmsnopg 5326
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.
StepHypRef Expression
1 vex 3060 . . . . . 6  |-  x  e. 
_V
2 vex 3060 . . . . . 6  |-  y  e. 
_V
31, 2opth1 4689 . . . . 5  |-  ( <.
x ,  y >.  =  <. A ,  B >.  ->  x  =  A )
43exlimiv 1787 . . . 4  |-  ( E. y <. x ,  y
>.  =  <. A ,  B >.  ->  x  =  A )
5 opeq1 4180 . . . . 5  |-  ( x  =  A  ->  <. x ,  B >.  =  <. A ,  B >. )
6 opeq2 4181 . . . . . . 7  |-  ( y  =  B  ->  <. x ,  y >.  =  <. x ,  B >. )
76eqeq1d 2464 . . . . . 6  |-  ( y  =  B  ->  ( <. x ,  y >.  =  <. A ,  B >.  <->  <. x ,  B >.  = 
<. A ,  B >. ) )
87spcegv 3147 . . . . 5  |-  ( B  e.  V  ->  ( <. x ,  B >.  = 
<. A ,  B >.  ->  E. y <. x ,  y
>.  =  <. A ,  B >. ) )
95, 8syl5 33 . . . 4  |-  ( B  e.  V  ->  (
x  =  A  ->  E. y <. x ,  y
>.  =  <. A ,  B >. ) )
104, 9impbid2 209 . . 3  |-  ( B  e.  V  ->  ( E. y <. x ,  y
>.  =  <. A ,  B >. 
<->  x  =  A ) )
111eldm2 5052 . . . 4  |-  ( x  e.  dom  { <. A ,  B >. }  <->  E. y <. x ,  y >.  e.  { <. A ,  B >. } )
12 opex 4678 . . . . . 6  |-  <. x ,  y >.  e.  _V
1312elsnc 4004 . . . . 5  |-  ( <.
x ,  y >.  e.  { <. A ,  B >. }  <->  <. x ,  y
>.  =  <. A ,  B >. )
1413exbii 1729 . . . 4  |-  ( E. y <. x ,  y
>.  e.  { <. A ,  B >. }  <->  E. y <. x ,  y >.  =  <. A ,  B >. )
1511, 14bitri 257 . . 3  |-  ( x  e.  dom  { <. A ,  B >. }  <->  E. y <. x ,  y >.  =  <. A ,  B >. )
16 elsn 3994 . . 3  |-  ( x  e.  { A }  <->  x  =  A )
1710, 15, 163bitr4g 296 . 2  |-  ( B  e.  V  ->  (
x  e.  dom  { <. A ,  B >. }  <-> 
x  e.  { A } ) )
1817eqrdv 2460 1  |-  ( B  e.  V  ->  dom  {
<. A ,  B >. }  =  { A }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   E.wex 1674    e. wcel 1898   {csn 3980   <.cop 3986   dom cdm 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-dm 4863
This theorem is referenced by:  dmsnopss  5327  dmpropg  5328  dmsnop  5329  rnsnopg  5334  fnsng  5648  funprg  5650  funtpg  5651  fntpg  5656  suppsnop  6955  funsnfsupp  7933  s1dmALT  12783  setsval  15195  estrreslem2  16072  eupap1  25753  bnj96  29725  bnj535  29750  snstriedgval  39184
  Copyright terms: Public domain W3C validator