Description: Obsolete version of 1oex as of 19-Sep-2024. (Contributed by BJ, 6-Apr-2019) (Proof shortened by AV, 1-Jul-2022) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 1oexOLD | ⊢ 1o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1on | ⊢ 1o ∈ On | |
2 | 1 | elexi | ⊢ 1o ∈ V |