Metamath Proof Explorer


Theorem 1ex

Description: One is a set. (Contributed by David A. Wheeler, 7-Jul-2016)

Ref Expression
Assertion 1ex
|- 1 e. _V

Proof

Step Hyp Ref Expression
1 ax-1cn
 |-  1 e. CC
2 1 elexi
 |-  1 e. _V