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  29255  wwlks2onv  30422  elwwlks2ons3im  30423  usgrwwlks2on  30427  umgrwwlks2on  30428  cyc3evpm  33592  prodfzo03  35113  circlevma  35152  circlemethhgt  35153  hgt750lemg  35164  hgt750lemb  35166  hgt750lema  35167  hgt750leme  35168  tgoldbachgtde  35170  tgoldbachgt  35173  usgrexmpl1tri  48943  usgrexmpl2nb0  48949  usgrexmpl2nb1  48950  usgrexmpl2nb2  48951