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

Theorem op1sta 5341
Description: Extract the first member of an ordered pair. (See op2nda 5344 to extract the second member, op1stb 4585 for an alternate version, and op1st 6591 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.)
Hypotheses
Ref Expression
cnvsn.1
cnvsn.2
Assertion
Ref Expression
op1sta

Proof of Theorem op1sta
StepHypRef Expression
1 cnvsn.2 . . . 4
21dmsnop 5333 . . 3
32unieqi 4126 . 2
4 cnvsn.1 . . 3
54unisn 4132 . 2
63, 5eqtri 2509 1
Colors of variables: wff set class
Syntax hints:  =wceq 1670  e.wcel 1732   cvv 3015  {csn 3909  <.cop 3912  U.cuni 4117  domcdm 4862
This theorem is referenced by:  elxp4  6530  op1st  6591  fo1st  6602  f1stres  6604  xpassen  7367  xpdom2  7368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-dm 4872
  Copyright terms: Public domain W3C validator