Theorem 0elpr01 11282

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

This proof depends on syntax axioms:   ∈ wcel 2145  {cpr 4586  0cc0 11181  1c1 11182

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 2733  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-i2m1 11249

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  prmreclem2  17075  i1f1lem  25990  i1f1  25991  cxplogb  27096  usgr2trlncl  30328  usgrwwlks2on  30529  umgrwwlks2on  30530  cyc3fv1  33680  constr01  34356  constrss  34357  constrconj  34359  constrelextdg2  34361  nn0constr  34375  fvrcllb0d  44652  fvrcllb0da  44653  corclrcl  44666  limsup10exlem  46726  stgr1  49003  gpgiedgdmellem  49088  gpgvtx0  49095  gpgprismgr4cycllem3  49139  gpgprismgr4cycllem9  49145  zlmodzxzscm  49413  2arympt  49705