Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
1oex
Next ⟩
2on
Metamath Proof Explorer
Ascii
Unicode
Theorem
1oex
Description:
Ordinal 1 is a set.
(Contributed by
BJ
, 6-Apr-2019)
(Proof shortened by
AV
, 1-Jul-2022)
Ref
Expression
Assertion
1oex
⊢
1
𝑜
∈
V
Proof
Step
Hyp
Ref
Expression
1
1on
⊢
1
𝑜
∈
On
2
1
elexi
⊢
1
𝑜
∈
V