Theorem tpid3 4741

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  {ctp 4595

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594  df-tp 4596

This theorem is used by:  hash3tpb  14546  wrdl3s3  15019  sgncl  15154  usgrwwlks2on  30350  umgrwwlks2on  30351  ex-pss  30826  cyc3evpm  33510  sgnsf  33522  prodfzo03  35031  circlevma  35070  circlemethhgt  35071  hgt750lemg  35082  hgt750lemb  35084  hgt750lema  35085  hgt750leme  35086  tgoldbachgtde  35088  tgoldbachgt  35091  kur14lem7  35717  brtpid3  36228  rabren3dioph  43575  oenord1ex  44075  fourierdlem114  46967  usgrexmpl1tri  48823  usgrexmpl2nb0  48829  usgrexmpl2nb1  48830  usgrexmpl2nb2  48831  usgrexmpl2nb3  48832  usgrexmpl2nb4  48833  usgrexmpl2nb5  48834  gpg3kgrtriex  48887