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

Theorem tpid1 4768
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 2737 . . 3 𝐴 = 𝐴
213mix1i 1334 . 2 (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶)
3 tpid1.1 . . 3 𝐴 ∈ V
43eltp 4689 . 2 (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶))
52, 4mpbir 231 1 𝐴 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1086   = wceq 1540  wcel 2108  Vcvv 3480  {ctp 4630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629  df-tp 4631
This theorem is referenced by:  tpnz  4779  hash3tpb  14534  wrdl3s3  15001  cffldtocusgr  29464  cffldtocusgrOLD  29465  umgrwwlks2on  29977  s3rnOLD  32930  cyc3evpm  33170  sgnsf  33182  sgncl  34541  prodfzo03  34618  circlevma  34657  circlemethhgt  34658  hgt750lemg  34669  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgt  34678  kur14lem7  35217  kur14lem9  35219  brtpid1  35721  rabren3dioph  42826  fourierdlem102  46223  fourierdlem114  46235  etransclem48  46297  usgrexmpl1tri  47984  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  gpg3kgrtriex  48045
  Copyright terms: Public domain W3C validator