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

Theorem op1sta 5320
Description: Extract the first member of an ordered pair. (See op2nda 5323 to extract the second member, op1stb 4569 for an alternate version, and op1st 6546 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 5312 . . 3
32unieqi 4110 . 2
4 cnvsn.1 . . 3
54unisn 4116 . 2
63, 5eqtri 2501 1
Colors of variables: wff set class
Syntax hints:  =wceq 1662  e.wcel 1724   cvv 3006  {csn 3894  <.cop 3897  U.cuni 4101  domcdm 4844
This theorem is referenced by:  elxp4  6485  op1st  6546  fo1st  6557  f1stres  6559  xpassen  7314  xpdom2  7315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pr 4538
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-rex 2757  df-rab 2760  df-v 3008  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-uni 4102  df-br 4303  df-dm 4854
  Copyright terms: Public domain W3C validator