Theorem 0elpr01 11331

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

This proof depends on syntax axioms:   ∈ wcel 2147  {cpr 4590  0cc0 11230  1c1 11231

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-mulcl 11292  ax-i2m1 11298

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  prmreclem2  17127  ehl2eudis  25776  i1f1lem  26043  i1f1  26044  cxplogb  27147  usgr2trlncl  30379  usgrwwlks2on  30580  umgrwwlks2on  30581  cyc3fv1  33774  constr01  34457  constrss  34458  constrconj  34460  constrelextdg2  34462  nn0constr  34476  fvrcllb0d  44896  fvrcllb0da  44897  corclrcl  44910  limsup10exlem  46997  stgr1  49274  gpgiedgdmellem  49359  gpgvtx0  49366  gpgprismgr4cycllem3  49410  gpgprismgr4cycllem9  49416  zlmodzxzscm  49684  2arympt  49976  rrx2pxel  50038