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

Theorem op1stb 4569
Description: Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 5322 to extract the second member, op1sta 5320 for an alternate version, and op1st 6546 for the preferred version.) (Contributed by NM, 25-Nov-2003.)
Hypotheses
Ref Expression
op1stb.1
op1stb.2
Assertion
Ref Expression
op1stb

Proof of Theorem op1stb
StepHypRef Expression
1 op1stb.1 . . . . . 6
2 op1stb.2 . . . . . 6
31, 2dfop 4068 . . . . 5
43inteqi 4142 . . . 4
5 snex 4540 . . . . . 6
6 prex 4541 . . . . . 6
75, 6intpr 4171 . . . . 5
8 snsspr1 4032 . . . . . 6
9 df-ss 3367 . . . . . 6
108, 9mpbi 201 . . . . 5
117, 10eqtri 2501 . . . 4
124, 11eqtri 2501 . . 3
1312inteqi 4142 . 2
141intsn 4174 . 2
1513, 14eqtri 2501 1
Colors of variables: wff set class
Syntax hints:  =wceq 1662  e.wcel 1724   cvv 3006  i^icin 3352  C_wss 3353  {csn 3894  {cpr 3895  <.cop 3897  |^|cint 4138
This theorem is referenced by:  elreldm  5068  op2ndb  5322  elxp5  6486  1stval2  6555  fundmen  7292  xpsnen  7304  xpnnenOLD  13278
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-ral 2756  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-int 4139
  Copyright terms: Public domain W3C validator