Theorem 1eltp012 12383

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

This proof depends on syntax axioms:   ∈ wcel 2145  {ctp 4587  0cc0 11172  1c1 11173  2c2 12367

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 2732  ax-1cn 11230

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3903  df-sn 4584  df-pr 4586  df-tp 4588

This theorem is used by:  s3rex  15069  wrdl3s3  15083  elcgrabasi  29309  wwlks2onv  30476  elwwlks2ons3im  30477  usgrwwlks2on  30481  umgrwwlks2on  30482  cyc3evpm  33645  prodfzo03  35167  circlevma  35206  circlemethhgt  35207  hgt750lemg  35218  hgt750lemb  35220  hgt750lema  35221  hgt750leme  35222  tgoldbachgtde  35224  tgoldbachgt  35227  usgrexmpl1tri  49045  usgrexmpl2nb0  49051  usgrexmpl2nb1  49052  usgrexmpl2nb2  49053