Theorem tpid3 4736

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  {ctp 4592

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591  df-tp 4593

This theorem is used by:  hash3tpb  14681  s3rex  15144  wrdl3s3  15158  sgncl  15293  degenmgm2nfun  19189  elcgrabasi  29432  usgrwwlks2on  30604  umgrwwlks2on  30605  ex-pss  31086  cyc3evpm  33810  sgnsf  33822  prodfzo03  35343  circlevma  35382  circlemethhgt  35383  hgt750lemg  35394  hgt750lemb  35396  hgt750lema  35397  hgt750leme  35398  tgoldbachgtde  35400  tgoldbachgt  35403  kur14lem7  36185  brtpid3  36703  rabren3dioph  44088  oenord1ex  44578  fourierdlem114  47503  usgrexmpl1tri  49396  usgrexmpl2nb0  49402  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  gpg3kgrtriex  49460