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

Theorem tpid2 4580
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 2779 . . 3 𝐵 = 𝐵
213mix2i 1314 . 2 (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶)
3 tpid2.1 . . 3 𝐵 ∈ V
43eltp 4500 . 2 (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶))
52, 4mpbir 223 1 𝐵 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1067   = wceq 1507  wcel 2050  Vcvv 3416  {ctp 4445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-v 3418  df-un 3835  df-sn 4442  df-pr 4444  df-tp 4446
This theorem is referenced by:  wrdl3s3  14187  wwlks2onv  27459  elwwlks2ons3im  27460  umgrwwlks2on  27463  s3rn  30364  sgnsf  30467  sgncl  31439  signsw0glem  31466  signsw0g  31469  signswmnd  31470  signswrid  31471  prodfzo03  31519  circlevma  31558  circlemethhgt  31559  hgt750lemg  31570  hgt750lemb  31572  hgt750lema  31573  hgt750leme  31574  tgoldbachgtde  31576  tgoldbachgt  31579  kur14lem7  32041  brtpid2  32469  rabren3dioph  38805  fourierdlem102  41922  fourierdlem114  41934  etransclem48  41996
  Copyright terms: Public domain W3C validator