Theorem tpid3 4769

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

Step	Hyp	Ref	Expression
1		tpid3.1	. 2 ⊢ 𝐶 ∈ V
2		tpid3g 4768	. 2 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶})
3	1, 2	ax-mp 5	1 ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∈ wcel 2098  Vcvv 3466  {ctp 4624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3945  df-sn 4621  df-pr 4623  df-tp 4625

This theorem is referenced by:  wrdl3s3  14910  umgrwwlks2on  29680  ex-pss  30150  s3rn  32579  cyc3evpm  32777  sgnsf  32789  sgncl  34026  prodfzo03  34104  circlevma  34143  circlemethhgt  34144  hgt750lemg  34155  hgt750lemb  34157  hgt750lema  34158  hgt750leme  34159  tgoldbachgtde  34161  tgoldbachgt  34164  kur14lem7  34692  brtpid3  35187  rabren3dioph  42042  oenord1ex  42554  fourierdlem114  45421