Theorem 1elpr01 11231

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 11230	. 2 ⊢ 1 ∈ V
2	1	prid2 4727	1 ⊢ 1 ∈ {0, 1}

This proof depends on syntax axioms:   ∈ wcel 2145  {cpr 4589  0cc0 11127  1c1 11128

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 2734  ax-1cn 11185

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  i1f1lem  25921  i1f1  25922  usgr2trlncl  30226  usgrwwlks2on  30427  umgrwwlks2on  30428  cyc3fv2  33580  esplyfvaln  34086  constrconj  34257  nn0constr  34273  fvrcllb1d  44537  relexp1idm  44556  corcltrcl  44581  cotrclrcl  44584  limsup10exlem  46602  stgr1  48879  gpgiedgdmellem  48964  gpgvtx1  48972  gpg3kgrtriex  49007  gpgprismgr4cycllem3  49015  gpgprismgr4cycllem9  49021  grlimedgnedg  49049  zlmodzxzscm  49289  2arympt  49581