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

Theorem tpid1 4684
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 1335 . 2 (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶)
3 tpid1.1 . . 3 𝐴 ∈ V
43eltp 4604 . 2 (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴𝐴 = 𝐵𝐴 = 𝐶))
52, 4mpbir 234 1 𝐴 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  w3o 1088   = wceq 1543  wcel 2110  Vcvv 3408  {ctp 4545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-sn 4542  df-pr 4544  df-tp 4546
This theorem is referenced by:  tpnz  4695  wrdl3s3  14529  cffldtocusgr  27535  umgrwwlks2on  28041  s3rn  30940  cyc3evpm  31136  sgnsf  31148  sgncl  32217  prodfzo03  32295  circlevma  32334  circlemethhgt  32335  hgt750lemg  32346  hgt750lemb  32348  hgt750lema  32349  hgt750leme  32350  tgoldbachgtde  32352  tgoldbachgt  32355  kur14lem7  32887  kur14lem9  32889  brtpid1  33380  rabren3dioph  40340  fourierdlem102  43424  fourierdlem114  43436  etransclem48  43498
  Copyright terms: Public domain W3C validator