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

Theorem tpid2 4698
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 𝐵 ∈ V
Assertion
Ref Expression
tpid2 𝐵 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid2
StepHypRef Expression
1 eqid 2818 . . 3 𝐵 = 𝐵
213mix2i 1326 . 2 (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶)
3 tpid2.1 . . 3 𝐵 ∈ V
43eltp 4618 . 2 (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶))
52, 4mpbir 232 1 𝐵 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1078   = wceq 1528  wcel 2105  Vcvv 3492  {ctp 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-sn 4558  df-pr 4560  df-tp 4562
This theorem is referenced by:  wrdl3s3  14314  wwlks2onv  27659  elwwlks2ons3im  27660  umgrwwlks2on  27663  s3rn  30549  cyc3evpm  30719  sgnsf  30731  sgncl  31695  signsw0glem  31722  signsw0g  31725  signswmnd  31726  signswrid  31727  prodfzo03  31773  circlevma  31812  circlemethhgt  31813  hgt750lemg  31824  hgt750lemb  31826  hgt750lema  31827  hgt750leme  31828  tgoldbachgtde  31830  tgoldbachgt  31833  kur14lem7  32356  brtpid2  32849  rabren3dioph  39290  fourierdlem102  42370  fourierdlem114  42382  etransclem48  42444
  Copyright terms: Public domain W3C validator