Theorem 1eltp012 12310

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

Syntax hints:   ∈ wcel 2141  {ctp 4592  0cc0 11099  1c1 11100  2c2 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4589  df-pr 4591  df-tp 4593

This theorem is referenced by:  wrdl3s3  14999  wwlks2onv  30268  elwwlks2ons3im  30269  usgrwwlks2on  30273  umgrwwlks2on  30274  cyc3evpm  33436  prodfzo03  34956  circlevma  34995  circlemethhgt  34996  hgt750lemg  35007  hgt750lemb  35009  hgt750lema  35010  hgt750leme  35011  tgoldbachgtde  35013  tgoldbachgt  35016  usgrexmpl1tri  48757  usgrexmpl2nb0  48763  usgrexmpl2nb1  48764  usgrexmpl2nb2  48765