Theorem tpid3 4727

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  {ctp 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580  df-tp 4582

This theorem is referenced by:  hash3tpb  14406  wrdl3s3  14873  usgrwwlks2on  29940  umgrwwlks2on  29941  ex-pss  30412  sgncl  32821  s3rnOLD  32936  cyc3evpm  33128  sgnsf  33140  prodfzo03  34639  circlevma  34678  circlemethhgt  34679  hgt750lemg  34690  hgt750lemb  34692  hgt750lema  34693  hgt750leme  34694  tgoldbachgtde  34696  tgoldbachgt  34699  kur14lem7  35279  brtpid3  35790  rabren3dioph  42935  oenord1ex  43435  fourierdlem114  46345  usgrexmpl1tri  48152  usgrexmpl2nb0  48158  usgrexmpl2nb1  48159  usgrexmpl2nb2  48160  usgrexmpl2nb3  48161  usgrexmpl2nb4  48162  usgrexmpl2nb5  48163  gpg3kgrtriex  48216