Theorem 1oelpr 8470

Description: 1_o is an element of {∅, 1_o}. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
1oelpr	⊢ 1o ∈ {∅, 1o}

Proof of Theorem 1oelpr

Step	Hyp	Ref	Expression
1		1oex 8469	. 2 ⊢ 1o ∈ V
2	1	prid2 4727	1 ⊢ 1o ∈ {∅, 1o}

This proof depends on syntax axioms:   ∈ wcel 2145  ∅c0 4282  {cpr 4589  1_oc1o 8452

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 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-un 3907  df-nul 4283  df-sn 4588  df-pr 4590  df-suc 6367  df-1o 8459

This theorem is used by:  nlim2  8481  djuss  9929  sadcf  16549  fnpr2ob  17650  setcepi  18183  setc2obas  18189  setc2ohom  18190  degenmgm  19056  degenmgm2  19059  efgi1  19854  frgpuptinv  19904  dprdpr  20185  xpstopnlem1  24041  xpstopnlem2  24043  omnord1ex  44153  oege2  44156  oenord1ex  44164  oenord1  44165  oaomoencom  44166  oenassex  44167  omcl3g  44183  clsk1indlem1  44893