Theorem 0elpr01 11202

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

Syntax hints:   ∈ wcel 2143  {cpr 4592  0cc0 11101  1c1 11102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-i2m1 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  prmreclem2  16978  i1f1lem  25829  i1f1  25830  cxplogb  26932  usgr2trlncl  30090  usgrwwlks2on  30288  umgrwwlks2on  30289  cyc3fv1  33438  constr01  34113  constrss  34114  constrconj  34116  constrelextdg2  34118  nn0constr  34132  fvrcllb0d  44402  fvrcllb0da  44403  corclrcl  44416  limsup10exlem  46469  stgr1  48709  gpgiedgdmellem  48794  gpgvtx0  48801  gpgprismgr4cycllem3  48845  gpgprismgr4cycllem9  48851  zlmodzxzscm  49120  2arympt  49412