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

Theorem tpid1 4664
 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 2798 . . 3 𝐴 = 𝐴
213mix1i 1330 . 2 (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶)
3 tpid1.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:  tpnz  4675  wrdl3s3  14320  cffldtocusgr  27247  umgrwwlks2on  27753  s3rn  30658  cyc3evpm  30852  sgnsf  30864  sgncl  31921  prodfzo03  31999  circlevma  32038  circlemethhgt  32039  hgt750lemg  32050  hgt750lemb  32052  hgt750lema  32053  hgt750leme  32054  tgoldbachgtde  32056  tgoldbachgt  32059  kur14lem7  32587  kur14lem9  32589  brtpid1  33079  rabren3dioph  39799  fourierdlem102  42893  fourierdlem114  42905  etransclem48  42967
 Copyright terms: Public domain W3C validator