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

Theorem tpid2 4274
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 2621 . . 3 𝐵 = 𝐵
213mix2i 1232 . 2 (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶)
3 tpid2.1 . . 3 𝐵 ∈ V
43eltp 4201 . 2 (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶))
52, 4mpbir 221 1 𝐵 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1035   = wceq 1480  wcel 1987  Vcvv 3186  {ctp 4152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-sn 4149  df-pr 4151  df-tp 4153
This theorem is referenced by:  wrdl3s3  13639  wwlks2onv  26716  elwwlks2ons3  26717  umgrwwlks2on  26719  sgnsf  29514  sgncl  30381  signsw0glem  30410  signsw0g  30413  signswmnd  30414  signswrid  30415  kur14lem7  30902  brtpid2  31312  rabren3dioph  36859  fourierdlem102  39732  fourierdlem114  39744  etransclem48  39806
  Copyright terms: Public domain W3C validator