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

Theorem tpid2 4117
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 2429 . . 3  |-  B  =  B
213mix2i 1178 . 2  |-  ( B  =  A  \/  B  =  B  \/  B  =  C )
3 tpid2.1 . . 3  |-  B  e. 
_V
43eltp 4048 . 2  |-  ( B  e.  { A ,  B ,  C }  <->  ( B  =  A  \/  B  =  B  \/  B  =  C )
)
52, 4mpbir 212 1  |-  B  e. 
{ A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 981    = wceq 1437    e. wcel 1870   _Vcvv 3087   {ctp 4006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-sn 4003  df-pr 4005  df-tp 4007
This theorem is referenced by:  2pthlem1  25170  2pthlem2  25171  el2wlkonotlem  25435  sgnsf  28330  sgncl  29197  signsw0glem  29230  signsw0g  29233  signswmnd  29234  signswrid  29235  kur14lem7  29723  brtpid2  30142  rabren3dioph  35367  fourierdlem102  37640  fourierdlem114  37652  etransclem48  37714
  Copyright terms: Public domain W3C validator