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

Theorem op1stb 4799
Description: Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 5399 to extract the second member, op1sta 5397 for an alternate version, and op1st 6405 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 4011 . . . . 5
43inteqi 4083 . . . 4
5 snex 4444 . . . . . 6
6 prex 4445 . . . . . 6
75, 6intpr 4112 . . . . 5
8 snsspr1 3975 . . . . . 6
9 df-ss 3323 . . . . . 6
108, 9mpbi 201 . . . . 5
117, 10eqtri 2463 . . . 4
124, 11eqtri 2463 . . 3
1312inteqi 4083 . 2
141intsn 4115 . 2
1513, 14eqtri 2463 1
Colors of variables: wff set class
Syntax hints:  =wceq 1654  e.wcel 1728   cvv 2965  i^icin 3308  C_wss 3309  {csn 3841  {cpr 3842  <.cop 3844  |^|cint 4079
This theorem is referenced by:  elreldm  5138  op2ndb  5399  elxp5  5404  1stval2  6414  fundmen  7229  xpsnen  7241  xpnnenOLD  12860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4364  ax-nul 4372  ax-pr 4442
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3766  df-sn 3847  df-pr 3848  df-op 3850  df-int 4080
  Copyright terms: Public domain W3C validator