Theorem 1elpr01 11276

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cpr 4585  0cc0 11172  1c1 11173

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 2732  ax-1cn 11230

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3903  df-sn 4584  df-pr 4586

This theorem is used by:  i1f1lem  25972  i1f1  25973  usgr2trlncl  30280  usgrwwlks2on  30481  umgrwwlks2on  30482  cyc3fv2  33633  esplyfvaln  34140  constrconj  34311  nn0constr  34327  fvrcllb1d  44639  relexp1idm  44658  corcltrcl  44683  cotrclrcl  44686  limsup10exlem  46704  stgr1  48981  gpgiedgdmellem  49066  gpgvtx1  49074  gpg3kgrtriex  49109  gpgprismgr4cycllem3  49117  gpgprismgr4cycllem9  49123  grlimedgnedg  49151  zlmodzxzscm  49391  2arympt  49683