Theorem tpid3 4732

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  {ctp 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585  df-tp 4587

This theorem is referenced by:  hash3tpb  14430  wrdl3s3  14897  usgrwwlks2on  30043  umgrwwlks2on  30044  ex-pss  30515  sgncl  32922  s3rnOLD  33038  cyc3evpm  33243  sgnsf  33255  prodfzo03  34780  circlevma  34819  circlemethhgt  34820  hgt750lemg  34831  hgt750lemb  34833  hgt750lema  34834  hgt750leme  34835  tgoldbachgtde  34837  tgoldbachgt  34840  kur14lem7  35425  brtpid3  35936  rabren3dioph  43169  oenord1ex  43669  fourierdlem114  46575  usgrexmpl1tri  48382  usgrexmpl2nb0  48388  usgrexmpl2nb1  48389  usgrexmpl2nb2  48390  usgrexmpl2nb3  48391  usgrexmpl2nb4  48392  usgrexmpl2nb5  48393  gpg3kgrtriex  48446