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

Theorem tpid2 4666
 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 2798 . . 3 𝐵 = 𝐵
213mix2i 1331 . 2 (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶)
3 tpid2.1 . . 3 𝐵 ∈ V
43eltp 4586 . 2 (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶))
52, 4mpbir 234 1 𝐵 ∈ {𝐴, 𝐵, 𝐶}
 Colors of variables: wff setvar class Syntax hints:   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {ctp 4529 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-tp 4530 This theorem is referenced by:  wrdl3s3  14319  wwlks2onv  27746  elwwlks2ons3im  27747  umgrwwlks2on  27750  s3rn  30655  cyc3evpm  30849  sgnsf  30861  sgncl  31918  signsw0glem  31945  signsw0g  31948  signswmnd  31949  signswrid  31950  prodfzo03  31996  circlevma  32035  circlemethhgt  32036  hgt750lemg  32047  hgt750lemb  32049  hgt750lema  32050  hgt750leme  32051  tgoldbachgtde  32053  tgoldbachgt  32056  kur14lem7  32584  brtpid2  33077  rabren3dioph  39771  fourierdlem102  42865  fourierdlem114  42877  etransclem48  42939
 Copyright terms: Public domain W3C validator