ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dmsnopg Unicode version

Theorem dmsnopg 4978
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 2661 . . . . . 6  |-  x  e. 
_V
2 vex 2661 . . . . . 6  |-  y  e. 
_V
31, 2opth1 4126 . . . . 5  |-  ( <.
x ,  y >.  =  <. A ,  B >.  ->  x  =  A )
43exlimiv 1560 . . . 4  |-  ( E. y <. x ,  y
>.  =  <. A ,  B >.  ->  x  =  A )
5 opeq1 3673 . . . . 5  |-  ( x  =  A  ->  <. x ,  B >.  =  <. A ,  B >. )
6 opeq2 3674 . . . . . . 7  |-  ( y  =  B  ->  <. x ,  y >.  =  <. x ,  B >. )
76eqeq1d 2124 . . . . . 6  |-  ( y  =  B  ->  ( <. x ,  y >.  =  <. A ,  B >.  <->  <. x ,  B >.  = 
<. A ,  B >. ) )
87spcegv 2746 . . . . 5  |-  ( B  e.  V  ->  ( <. x ,  B >.  = 
<. A ,  B >.  ->  E. y <. x ,  y
>.  =  <. A ,  B >. ) )
95, 8syl5 32 . . . 4  |-  ( B  e.  V  ->  (
x  =  A  ->  E. y <. x ,  y
>.  =  <. A ,  B >. ) )
104, 9impbid2 142 . . 3  |-  ( B  e.  V  ->  ( E. y <. x ,  y
>.  =  <. A ,  B >. 
<->  x  =  A ) )
111eldm2 4705 . . . 4  |-  ( x  e.  dom  { <. A ,  B >. }  <->  E. y <. x ,  y >.  e.  { <. A ,  B >. } )
121, 2opex 4119 . . . . . 6  |-  <. x ,  y >.  e.  _V
1312elsn 3511 . . . . 5  |-  ( <.
x ,  y >.  e.  { <. A ,  B >. }  <->  <. x ,  y
>.  =  <. A ,  B >. )
1413exbii 1567 . . . 4  |-  ( E. y <. x ,  y
>.  e.  { <. A ,  B >. }  <->  E. y <. x ,  y >.  =  <. A ,  B >. )
1511, 14bitri 183 . . 3  |-  ( x  e.  dom  { <. A ,  B >. }  <->  E. y <. x ,  y >.  =  <. A ,  B >. )
16 velsn 3512 . . 3  |-  ( x  e.  { A }  <->  x  =  A )
1710, 15, 163bitr4g 222 . 2  |-  ( B  e.  V  ->  (
x  e.  dom  { <. A ,  B >. }  <-> 
x  e.  { A } ) )
1817eqrdv 2113 1  |-  ( B  e.  V  ->  dom  {
<. A ,  B >. }  =  { A }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314   E.wex 1451    e. wcel 1463   {csn 3495   <.cop 3498   dom cdm 4507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-br 3898  df-dm 4517
This theorem is referenced by:  dmpropg  4979  dmsnop  4980  rnsnopg  4985  elxp4  4994  fnsng  5138  funprg  5141  funtpg  5142  fntpg  5147  ennnfonelemhdmp1  11828  ennnfonelemkh  11831  setsvala  11896  setsresg  11903  setscom  11905  setsslid  11915  strle1g  11955
  Copyright terms: Public domain W3C validator