Theorem 0elpr01 11219

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

This proof depends on syntax axioms:   ∈ wcel 2146  {cpr 4596  0cc0 11118  1c1 11119

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 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-i2m1 11186

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  prmreclem2  17002  i1f1lem  25885  i1f1  25886  cxplogb  26988  usgr2trlncl  30146  usgrwwlks2on  30344  umgrwwlks2on  30345  cyc3fv1  33488  constr01  34163  constrss  34164  constrconj  34166  constrelextdg2  34168  nn0constr  34182  fvrcllb0d  44460  fvrcllb0da  44461  corclrcl  44474  limsup10exlem  46527  stgr1  48767  gpgiedgdmellem  48852  gpgvtx0  48859  gpgprismgr4cycllem3  48903  gpgprismgr4cycllem9  48909  zlmodzxzscm  49178  2arympt  49470