Theorem 1eltp012 12338

Description: 1 is an element of {0, 1, 2}. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
1eltp012	⊢ 1 ∈ {0, 1, 2}

Proof of Theorem 1eltp012

Step	Hyp	Ref	Expression
1		1ex 11230	. 2 ⊢ 1 ∈ V
2	1	tpid2 4734	1 ⊢ 1 ∈ {0, 1, 2}

This proof depends on syntax axioms:   ∈ wcel 2145  {ctp 4591  0cc0 11127  1c1 11128  2c2 12322

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 2734  ax-1cn 11185

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590  df-tp 4592

This theorem is used by:  s3rex  15023  wrdl3s3  15037  elcgrabasi  29250  wwlks2onv  30407  elwwlks2ons3im  30408  usgrwwlks2on  30412  umgrwwlks2on  30413  cyc3evpm  33577  prodfzo03  35098  circlevma  35137  circlemethhgt  35138  hgt750lemg  35149  hgt750lemb  35151  hgt750lema  35152  hgt750leme  35153  tgoldbachgtde  35155  tgoldbachgt  35158  usgrexmpl1tri  48928  usgrexmpl2nb0  48934  usgrexmpl2nb1  48935  usgrexmpl2nb2  48936