Theorem tpid3 4739

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {ctp 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592  df-tp 4594

This theorem is referenced by:  hash3tpb  14528  wrdl3s3  14995  sgncl  15130  usgrwwlks2on  30307  umgrwwlks2on  30308  ex-pss  30779  s3rnOLD  33266  cyc3evpm  33470  sgnsf  33482  prodfzo03  34990  circlevma  35029  circlemethhgt  35030  hgt750lemg  35041  hgt750lemb  35043  hgt750lema  35044  hgt750leme  35045  tgoldbachgtde  35047  tgoldbachgt  35050  kur14lem7  35704  brtpid3  36215  rabren3dioph  43542  oenord1ex  44042  fourierdlem114  46934  usgrexmpl1tri  48790  usgrexmpl2nb0  48796  usgrexmpl2nb1  48797  usgrexmpl2nb2  48798  usgrexmpl2nb3  48799  usgrexmpl2nb4  48800  usgrexmpl2nb5  48801  gpg3kgrtriex  48854