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

Theorem tpid3 4721
Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 30-Apr-2021.)
Hypothesis
Ref Expression
tpid3.1 𝐶 ∈ V
Assertion
Ref Expression
tpid3 𝐶 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid3
StepHypRef Expression
1 tpid3.1 . 2 𝐶 ∈ V
2 tpid3g 4720 . 2 (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶})
31, 2ax-mp 5 1 𝐶 ∈ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3441  {ctp 4577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-un 3903  df-sn 4574  df-pr 4576  df-tp 4578
This theorem is referenced by:  wrdl3s3  14776  umgrwwlks2on  28610  ex-pss  29080  s3rn  31507  cyc3evpm  31704  sgnsf  31716  sgncl  32805  prodfzo03  32883  circlevma  32922  circlemethhgt  32923  hgt750lemg  32934  hgt750lemb  32936  hgt750lema  32937  hgt750leme  32938  tgoldbachgtde  32940  tgoldbachgt  32943  kur14lem7  33473  brtpid3  33964  rabren3dioph  40899  fourierdlem114  44097
  Copyright terms: Public domain W3C validator