Theorem tpid3 4734

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  {ctp 4588

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587  df-tp 4589

This theorem is used by:  hash3tpb  14560  s3rex  15021  wrdl3s3  15035  sgncl  15170  degenmgm2nfun  19052  elcgrabasi  29254  usgrwwlks2on  30426  umgrwwlks2on  30427  ex-pss  30908  cyc3evpm  33590  sgnsf  33602  prodfzo03  35111  circlevma  35150  circlemethhgt  35151  hgt750lemg  35162  hgt750lemb  35164  hgt750lema  35165  hgt750leme  35166  tgoldbachgtde  35168  tgoldbachgt  35171  kur14lem7  35791  brtpid3  36302  rabren3dioph  43656  oenord1ex  44156  fourierdlem114  47048  usgrexmpl1tri  48941  usgrexmpl2nb0  48947  usgrexmpl2nb1  48948  usgrexmpl2nb2  48949  usgrexmpl2nb3  48950  usgrexmpl2nb4  48951  usgrexmpl2nb5  48952  gpg3kgrtriex  49005