Metamath Proof Explorer

Theorem hlex

Description: The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hlex.1 
|- X = ( BaseSet ` U )
Assertion hlex 
|- X e. _V

Proof

Step Hyp Ref Expression
1 hlex.1 
 |-  X = ( BaseSet ` U )
2 1 fvexi 
 |-  X e. _V