Theorem 1oelpr 8490

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 8489	. 2 ⊢ 1o ∈ V
2	1	prid2 4720	1 ⊢ 1o ∈ {∅, 1o}

This proof depends on syntax axioms:   ∈ wcel 2144  ∅c0 4278  {cpr 4586  1_oc1o 8472

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-pr 4587  df-suc 6368  df-1o 8479

This theorem is used by:  nlim2  8501  djuss  10004  sadcf  16628  fnpr2ob  17735  setcepi  18268  setc2obas  18274  setc2ohom  18275  degenmgm  19142  degenmgm2  19145  efgi1  19940  frgpuptinv  19990  dprdpr  20271  xpstopnlem1  24133  xpstopnlem2  24135  omnord1ex  44399  oege2  44402  oenord1ex  44410  oenord1  44411  oaomoencom  44412  oenassex  44413  omcl3g  44429  clsk1indlem1  45138  parswapprop  50870  par2hom  50872  par2diag  50873  fuconuniqlem  50874  fuconuniqvalslem  50876