Theorem 1elpr01 11305

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

This proof depends on syntax axioms:   ∈ wcel 2144  {cpr 4585  0cc0 11201  1c1 11202

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4584  df-pr 4586

This theorem is used by:  i1f1lem  26011  i1f1  26012  usgr2trlncl  30347  usgrwwlks2on  30548  umgrwwlks2on  30549  cyc3fv2  33742  esplyfvaln  34249  constrconj  34420  nn0constr  34436  fvrcllb1d  44771  relexp1idm  44790  corcltrcl  44815  cotrclrcl  44818  limsup10exlem  46858  stgr1  49135  gpgiedgdmellem  49220  gpgvtx1  49228  gpg3kgrtriex  49263  gpgprismgr4cycllem3  49271  gpgprismgr4cycllem9  49277  grlimedgnedg  49305  zlmodzxzscm  49545  2arympt  49837