Theorem tpid3 4725

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  {ctp 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580  df-tp 4582

This theorem is referenced by:  hash3tpb  14402  wrdl3s3  14869  umgrwwlks2on  29902  ex-pss  30372  sgncl  32777  s3rnOLD  32888  cyc3evpm  33093  sgnsf  33105  prodfzo03  34577  circlevma  34616  circlemethhgt  34617  hgt750lemg  34628  hgt750lemb  34630  hgt750lema  34631  hgt750leme  34632  tgoldbachgtde  34634  tgoldbachgt  34637  kur14lem7  35195  brtpid3  35706  rabren3dioph  42798  oenord1ex  43298  fourierdlem114  46211  usgrexmpl1tri  48019  usgrexmpl2nb0  48025  usgrexmpl2nb1  48026  usgrexmpl2nb2  48027  usgrexmpl2nb3  48028  usgrexmpl2nb4  48029  usgrexmpl2nb5  48030  gpg3kgrtriex  48083