Theorem 0elpr01 11301

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

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

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 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-i2m1 11268

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  17095  i1f1lem  26010  i1f1  26011  cxplogb  27114  usgr2trlncl  30346  usgrwwlks2on  30547  umgrwwlks2on  30548  cyc3fv1  33698  constr01  34374  constrss  34375  constrconj  34377  constrelextdg2  34379  nn0constr  34393  fvrcllb0d  44692  fvrcllb0da  44693  corclrcl  44706  limsup10exlem  46781  stgr1  49058  gpgiedgdmellem  49143  gpgvtx0  49150  gpgprismgr4cycllem3  49194  gpgprismgr4cycllem9  49200  zlmodzxzscm  49468  2arympt  49760