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

Theorem tpid1 4488
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
tpid1.1 𝐴 ∈ V
Assertion
Ref Expression
tpid1 𝐴 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid1
StepHypRef Expression
1 eqid 2802 . . 3 𝐴 = 𝐴
213mix1i 1425 . 2 (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶)
3 tpid1.1 . . 3 𝐴 ∈ V
43eltp 4416 . 2 (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶))
52, 4mpbir 222 1 𝐴 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1099   = wceq 1637  wcel 2155  Vcvv 3387  {ctp 4368
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 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
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 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-un 3768  df-sn 4365  df-pr 4367  df-tp 4369
This theorem is referenced by:  tpnz  4496  wrdl3s3  13924  cffldtocusgr  26565  umgrwwlks2on  27092  sgnsf  30048  sgncl  30919  prodfzo03  31000  circlevma  31039  circlemethhgt  31040  hgt750lemg  31051  hgt750lemb  31053  hgt750lema  31054  hgt750leme  31055  tgoldbachgtde  31057  tgoldbachgt  31060  kur14lem7  31511  kur14lem9  31513  brtpid1  31918  rabren3dioph  37875  fourierdlem102  40898  fourierdlem114  40910  etransclem48  40972
  Copyright terms: Public domain W3C validator