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

Theorem tpid2 4130
Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Hypothesis
Ref Expression
tpid2.1  |-  B  e. 
_V
Assertion
Ref Expression
tpid2  |-  B  e. 
{ A ,  B ,  C }

Proof of Theorem tpid2
StepHypRef Expression
1 eqid 2454 . . 3  |-  B  =  B
213mix2i 1167 . 2  |-  ( B  =  A  \/  B  =  B  \/  B  =  C )
3 tpid2.1 . . 3  |-  B  e. 
_V
43eltp 4061 . 2  |-  ( B  e.  { A ,  B ,  C }  <->  ( B  =  A  \/  B  =  B  \/  B  =  C )
)
52, 4mpbir 209 1  |-  B  e. 
{ A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 970    = wceq 1398    e. wcel 1823   _Vcvv 3106   {ctp 4020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-sn 4017  df-pr 4019  df-tp 4021
This theorem is referenced by:  2pthlem1  24802  2pthlem2  24803  el2wlkonotlem  25067  sgnsf  27956  sgncl  28744  signsw0glem  28777  signsw0g  28780  signswmnd  28781  signswrid  28782  kur14lem7  28923  brtpid2  29343  rabren3dioph  30991  fourierdlem102  32233  fourierdlem114  32245  etransclem48  32307
  Copyright terms: Public domain W3C validator