Theorem 1oelpr 8473

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

This proof depends on syntax axioms:   ∈ wcel 2146  ∅c0 4289  {cpr 4596  1_oc1o 8455

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-un 3913  df-nul 4290  df-sn 4595  df-pr 4597  df-suc 6373  df-1o 8462

This theorem is used by:  nlim2  8484  djuss  9925  sadcf  16536  fnpr2ob  17637  setcepi  18170  setc2obas  18176  setc2ohom  18177  efgi1  19816  frgpuptinv  19866  dprdpr  20147  xpstopnlem1  23996  xpstopnlem2  23998  omnord1ex  44064  oege2  44067  oenord1ex  44075  oenord1  44076  oaomoencom  44077  oenassex  44078  omcl3g  44094  clsk1indlem1  44804