Theorem tpid3 4714

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

Syntax hints:   ∈ wcel 2109  Vcvv 3430  {ctp 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-sn 4567  df-pr 4569  df-tp 4571

This theorem is referenced by:  wrdl3s3  14658  umgrwwlks2on  28301  ex-pss  28771  s3rn  31199  cyc3evpm  31396  sgnsf  31408  sgncl  32484  prodfzo03  32562  circlevma  32601  circlemethhgt  32602  hgt750lemg  32613  hgt750lemb  32615  hgt750lema  32616  hgt750leme  32617  tgoldbachgtde  32619  tgoldbachgt  32622  kur14lem7  33153  brtpid3  33646  rabren3dioph  40617  fourierdlem114  43715