Theorem 1elpr01 11222

Description: 1 is an element of {0, 1}. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
1elpr01	⊢ 1 ∈ {0, 1}

Proof of Theorem 1elpr01

Step	Hyp	Ref	Expression
1		1ex 11221	. 2 ⊢ 1 ∈ V
2	1	prid2 4734	1 ⊢ 1 ∈ {0, 1}

This proof depends on syntax axioms:   ∈ wcel 2146  {cpr 4596  0cc0 11118  1c1 11119

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 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  i1f1lem  25885  i1f1  25886  usgr2trlncl  30146  usgrwwlks2on  30344  umgrwwlks2on  30345  cyc3fv2  33489  esplyfvaln  33995  constrconj  34166  nn0constr  34182  fvrcllb1d  44461  relexp1idm  44480  corcltrcl  44505  cotrclrcl  44508  limsup10exlem  46526  stgr1  48766  gpgiedgdmellem  48851  gpgvtx1  48859  gpg3kgrtriex  48894  gpgprismgr4cycllem3  48902  gpgprismgr4cycllem9  48908  grlimedgnedg  48936  zlmodzxzscm  49177  2arympt  49469