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

Theorem op1sta 5275
Description: Extract the first member of an ordered pair. (See op2nda 5278 to extract the second member, op1stb 4629 for an alternate version, and op1st 6754 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
Hypotheses
Ref Expression
cnvsn.1  |-  A  e. 
_V
cnvsn.2  |-  B  e. 
_V
Assertion
Ref Expression
op1sta  |-  U. dom  {
<. A ,  B >. }  =  A

Proof of Theorem op1sta
StepHypRef Expression
1 cnvsn.2 . . . 4  |-  B  e. 
_V
21dmsnop 5267 . . 3  |-  dom  { <. A ,  B >. }  =  { A }
32unieqi 4166 . 2  |-  U. dom  {
<. A ,  B >. }  =  U. { A }
4 cnvsn.1 . . 3  |-  A  e. 
_V
54unisn 4172 . 2  |-  U. { A }  =  A
63, 5eqtri 2445 1  |-  U. dom  {
<. A ,  B >. }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872   _Vcvv 3017   {csn 3936   <.cop 3942   U.cuni 4157   dom cdm 4791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-dm 4801
This theorem is referenced by:  elxp4  6690  op1st  6754  fo1st  6766  f1stres  6768  xpassen  7614  xpdom2  7615
  Copyright terms: Public domain W3C validator