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

Theorem tpid2 4506
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 2817 . . 3 𝐵 = 𝐵
213mix2i 1426 . 2 (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶)
3 tpid2.1 . . 3 𝐵 ∈ V
43eltp 4433 . 2 (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴𝐵 = 𝐵𝐵 = 𝐶))
52, 4mpbir 222 1 𝐵 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1099   = wceq 1637  wcel 2157  Vcvv 3402  {ctp 4385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-un 3785  df-sn 4382  df-pr 4384  df-tp 4386
This theorem is referenced by:  wrdl3s3  13950  wwlks2onv  27116  elwwlks2ons3im  27117  elwwlks2ons3OLD  27119  umgrwwlks2on  27121  sgnsf  30077  sgncl  30948  signsw0glem  30978  signsw0g  30981  signswmnd  30982  signswrid  30983  prodfzo03  31029  circlevma  31068  circlemethhgt  31069  hgt750lemg  31080  hgt750lemb  31082  hgt750lema  31083  hgt750leme  31084  tgoldbachgtde  31086  tgoldbachgt  31089  kur14lem7  31539  brtpid2  31947  rabren3dioph  37899  fourierdlem102  40922  fourierdlem114  40934  etransclem48  40996
  Copyright terms: Public domain W3C validator