Theorem tpid3 4730

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587  df-tp 4589

This theorem is used by:  hash3tpb  14644  s3rex  15107  wrdl3s3  15121  sgncl  15256  degenmgm2nfun  19145  elcgrabasi  29381  usgrwwlks2on  30553  umgrwwlks2on  30554  ex-pss  31035  cyc3evpm  33758  sgnsf  33770  prodfzo03  35279  circlevma  35318  circlemethhgt  35319  hgt750lemg  35330  hgt750lemb  35332  hgt750lema  35333  hgt750leme  35334  tgoldbachgtde  35336  tgoldbachgt  35339  kur14lem7  36064  brtpid3  36581  rabren3dioph  43916  oenord1ex  44411  fourierdlem114  47324  usgrexmpl1tri  49217  usgrexmpl2nb0  49223  usgrexmpl2nb1  49224  usgrexmpl2nb2  49225  usgrexmpl2nb3  49226  usgrexmpl2nb4  49227  usgrexmpl2nb5  49228  gpg3kgrtriex  49281