Theorem tpid3 4705

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  {ctp 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-pr 4558  df-tp 4560

This theorem is referenced by:  hash3tpb  14448  wrdl3s3  14915  usgrwwlks2on  30044  umgrwwlks2on  30045  ex-pss  30516  sgncl  32923  s3rnOLD  33025  cyc3evpm  33231  sgnsf  33243  prodfzo03  34787  circlevma  34826  circlemethhgt  34827  hgt750lemg  34838  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  tgoldbachgtde  34844  tgoldbachgt  34847  kur14lem7  35440  brtpid3  35951  rabren3dioph  43260  oenord1ex  43760  fourierdlem114  46663  usgrexmpl1tri  48516  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  gpg3kgrtriex  48580