Theorem tpid3 4709

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

Syntax hints:   ∈ wcel 2106  Vcvv 3429  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3431  df-un 3891  df-sn 4562  df-pr 4564  df-tp 4566

This theorem is referenced by:  wrdl3s3  14687  umgrwwlks2on  28330  ex-pss  28800  s3rn  31228  cyc3evpm  31425  sgnsf  31437  sgncl  32513  prodfzo03  32591  circlevma  32630  circlemethhgt  32631  hgt750lemg  32642  hgt750lemb  32644  hgt750lema  32645  hgt750leme  32646  tgoldbachgtde  32648  tgoldbachgt  32651  kur14lem7  33182  brtpid3  33675  rabren3dioph  40645  fourierdlem114  43742