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

Theorem tpid1 4772
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 2734 . . 3 𝐴 = 𝐴
213mix1i 1332 . 2 (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶)
3 tpid1.1 . . 3 𝐴 ∈ V
43eltp 4693 . 2 (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶))
52, 4mpbir 231 1 𝐴 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1085   = wceq 1536  wcel 2105  Vcvv 3477  {ctp 4634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-pr 4633  df-tp 4635
This theorem is referenced by:  tpnz  4783  hash3tpb  14530  wrdl3s3  14997  cffldtocusgr  29478  cffldtocusgrOLD  29479  umgrwwlks2on  29986  s3rnOLD  32914  cyc3evpm  33152  sgnsf  33164  sgncl  34519  prodfzo03  34596  circlevma  34635  circlemethhgt  34636  hgt750lemg  34647  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgt  34656  kur14lem7  35196  kur14lem9  35198  brtpid1  35700  rabren3dioph  42802  fourierdlem102  46163  fourierdlem114  46175  etransclem48  46237  usgrexmpl1tri  47919  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930
  Copyright terms: Public domain W3C validator