Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Ordinals
elong
Next ⟩
elon
Metamath Proof Explorer
Ascii
Unicode
Theorem
elong
Description:
An ordinal number is an ordinal set.
(Contributed by
NM
, 5-Jun-1994)
Ref
Expression
Assertion
elong
⊢
A
∈
V
→
A
∈
On
↔
Ord
⁡
A
Proof
Step
Hyp
Ref
Expression
1
ordeq
⊢
y
=
x
→
Ord
⁡
y
↔
Ord
⁡
x
2
ordeq
⊢
x
=
A
→
Ord
⁡
x
↔
Ord
⁡
A
3
df-on
⊢
On
=
y
|
Ord
⁡
y
4
1
2
3
elab2gw
⊢
A
∈
V
→
A
∈
On
↔
Ord
⁡
A