Theorem tpid3 4722

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

Syntax hints:   ∈ wcel 2132  Vcvv 3444  {ctp 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-un 3900  df-sn 4573  df-pr 4575  df-tp 4577

This theorem is referenced by:  hash3tpb  14494  wrdl3s3  14961  usgrwwlks2on  30093  umgrwwlks2on  30094  ex-pss  30565  sgncl  32972  s3rnOLD  33074  cyc3evpm  33280  sgnsf  33292  prodfzo03  34844  circlevma  34883  circlemethhgt  34884  hgt750lemg  34895  hgt750lemb  34897  hgt750lema  34898  hgt750leme  34899  tgoldbachgtde  34901  tgoldbachgt  34904  kur14lem7  35500  brtpid3  36011  rabren3dioph  43330  oenord1ex  43830  fourierdlem114  46732  usgrexmpl1tri  48585  usgrexmpl2nb0  48591  usgrexmpl2nb1  48592  usgrexmpl2nb2  48593  usgrexmpl2nb3  48594  usgrexmpl2nb4  48595  usgrexmpl2nb5  48596  gpg3kgrtriex  48649