Theorem 1eltp012 12414

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 11304	. 2 ⊢ 1 ∈ V
2	1	tpid2 4730	1 ⊢ 1 ∈ {0, 1, 2}

This proof depends on syntax axioms:   ∈ wcel 2144  {ctp 4587  0cc0 11201  1c1 11202  2c2 12398

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  ax-1cn 11259

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 4584  df-pr 4586  df-tp 4588

This theorem is used by:  s3rex  15102  wrdl3s3  15116  elcgrabasi  29376  wwlks2onv  30543  elwwlks2ons3im  30544  usgrwwlks2on  30548  umgrwwlks2on  30549  cyc3evpm  33754  prodfzo03  35275  circlevma  35314  circlemethhgt  35315  hgt750lemg  35326  hgt750lemb  35328  hgt750lema  35329  hgt750leme  35330  tgoldbachgtde  35332  tgoldbachgt  35335  usgrexmpl1tri  49199  usgrexmpl2nb0  49205  usgrexmpl2nb1  49206  usgrexmpl2nb2  49207