Theorem 1oelpr 8463

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

Syntax hints:   ∈ wcel 2141  ∅c0 4285  {cpr 4590  1_oc1o 8445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-un 3909  df-nul 4286  df-sn 4589  df-pr 4591  df-suc 6366  df-1o 8452

This theorem is referenced by:  nlim2  8474  djuss  9905  sadcf  16510  fnpr2ob  17611  setcepi  18144  setc2obas  18150  setc2ohom  18151  efgi1  19790  frgpuptinv  19840  dprdpr  20121  xpstopnlem1  23945  xpstopnlem2  23947  omnord1ex  44001  oege2  44004  oenord1ex  44012  oenord1  44013  oaomoencom  44014  oenassex  44015  omcl3g  44031  clsk1indlem1  44741