Theorem tpid3 4734

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  {ctp 4588

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587  df-tp 4589

This theorem is used by:  hash3tpb  14633  s3rex  15094  wrdl3s3  15108  sgncl  15243  degenmgm2nfun  19132  elcgrabasi  29368  usgrwwlks2on  30540  umgrwwlks2on  30541  ex-pss  31022  cyc3evpm  33704  sgnsf  33716  prodfzo03  35225  circlevma  35264  circlemethhgt  35265  hgt750lemg  35276  hgt750lemb  35278  hgt750lema  35279  hgt750leme  35280  tgoldbachgtde  35282  tgoldbachgt  35285  kur14lem7  35956  brtpid3  36467  rabren3dioph  43801  oenord1ex  44301  fourierdlem114  47199  usgrexmpl1tri  49092  usgrexmpl2nb0  49098  usgrexmpl2nb1  49099  usgrexmpl2nb2  49100  usgrexmpl2nb3  49101  usgrexmpl2nb4  49102  usgrexmpl2nb5  49103  gpg3kgrtriex  49156