Theorem 1eltp012 12440

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

This proof depends on syntax axioms:   ∈ wcel 2147  {ctp 4592  0cc0 11227  1c1 11228  2c2 12424

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591  df-tp 4593

This theorem is used by:  s3rex  15130  wrdl3s3  15144  elcgrabasi  29405  wwlks2onv  30572  elwwlks2ons3im  30573  usgrwwlks2on  30577  umgrwwlks2on  30578  cyc3evpm  33781  prodfzo03  35302  circlevma  35341  circlemethhgt  35342  hgt750lemg  35353  hgt750lemb  35355  hgt750lema  35356  hgt750leme  35357  tgoldbachgtde  35359  tgoldbachgt  35362  usgrexmpl1tri  49328  usgrexmpl2nb0  49334  usgrexmpl2nb1  49335  usgrexmpl2nb2  49336