Theorem 1elpr01 11203

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

Syntax hints:   ∈ wcel 2141  {cpr 4590  0cc0 11099  1c1 11100

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-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

This theorem is referenced by:  i1f1lem  25827  i1f1  25828  usgr2trlncl  30075  usgrwwlks2on  30273  umgrwwlks2on  30274  cyc3fv2  33424  esplyfvaln  33930  constrconj  34101  nn0constr  34117  fvrcllb1d  44391  relexp1idm  44410  corcltrcl  44435  cotrclrcl  44438  limsup10exlem  46456  stgr1  48693  gpgiedgdmellem  48778  gpgvtx1  48786  gpg3kgrtriex  48821  gpgprismgr4cycllem3  48829  gpgprismgr4cycllem9  48835  grlimedgnedg  48863  zlmodzxzscm  49104  2arympt  49396