Theorem 0elpr01 11305

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

Assertion

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

Proof of Theorem 0elpr01

Step	Hyp	Ref	Expression
1		c0ex 11304	. 2 ⊢ 0 ∈ V
2	1	prid1 4719	1 ⊢ 0 ∈ {0, 1}

This proof depends on syntax axioms:   ∈ wcel 2144  {cpr 4586  0cc0 11204  1c1 11205

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 11262  ax-icn 11263  ax-addcl 11264  ax-mulcl 11266  ax-i2m1 11272

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 4585  df-pr 4587

This theorem is used by:  prmreclem2  17101  ehl2eudis  25749  i1f1lem  26016  i1f1  26017  cxplogb  27120  usgr2trlncl  30352  usgrwwlks2on  30553  umgrwwlks2on  30554  cyc3fv1  33745  constr01  34421  constrss  34422  constrconj  34424  constrelextdg2  34426  nn0constr  34440  fvrcllb0d  44787  fvrcllb0da  44788  corclrcl  44801  limsup10exlem  46876  stgr1  49153  gpgiedgdmellem  49238  gpgvtx0  49245  gpgprismgr4cycllem3  49289  gpgprismgr4cycllem9  49295  zlmodzxzscm  49563  2arympt  49855  rrx2pxel  49917  2sphere0  49956