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

Theorem tpid2 4717
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 2736 . . 3 𝐵 = 𝐵
213mix2i 1333 . 2 (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶)
3 tpid2.1 . . 3 𝐵 ∈ V
43eltp 4635 . 2 (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶))
52, 4mpbir 230 1 𝐵 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1085   = wceq 1540  wcel 2105  Vcvv 3441  {ctp 4576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-un 3902  df-sn 4573  df-pr 4575  df-tp 4577
This theorem is referenced by:  wrdl3s3  14768  wwlks2onv  28547  elwwlks2ons3im  28548  umgrwwlks2on  28551  s3rn  31448  cyc3evpm  31645  sgnsf  31657  sgncl  32746  signsw0glem  32773  signsw0g  32776  signswmnd  32777  signswrid  32778  prodfzo03  32824  circlevma  32863  circlemethhgt  32864  hgt750lemg  32875  hgt750lemb  32877  hgt750lema  32878  hgt750leme  32879  tgoldbachgtde  32881  tgoldbachgt  32884  kur14lem7  33414  brtpid2  33904  rabren3dioph  40887  fourierdlem102  44074  fourierdlem114  44086  etransclem48  44148
  Copyright terms: Public domain W3C validator