Theorem tpid3 4777

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 4776	. 2 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶})
3	1, 2	ax-mp 5	1 ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∈ 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:  hash3tpb  14530  wrdl3s3  14997  umgrwwlks2on  29986  ex-pss  30456  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  brtpid3  35702  rabren3dioph  42802  oenord1ex  43304  fourierdlem114  46175  usgrexmpl1tri  47919  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930