Theorem tpid3 4737

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  {ctp 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592  df-tp 4594

This theorem is referenced by:  hash3tpb  14460  wrdl3s3  14928  umgrwwlks2on  29887  ex-pss  30357  sgncl  32756  s3rnOLD  32867  cyc3evpm  33107  sgnsf  33119  prodfzo03  34594  circlevma  34633  circlemethhgt  34634  hgt750lemg  34645  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  kur14lem7  35199  brtpid3  35710  rabren3dioph  42803  oenord1ex  43304  fourierdlem114  46218  usgrexmpl1tri  48016  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  gpg3kgrtriex  48080