Axiom ax-hilex

Description: This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. We assume that there exists a primitive class, ~H , which contains objects called vectors. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chba	$$class\mathscr{H}$$
1		cvv	$$class\mathrm{V}$$
2	0 1	wcel	$$wff\mathscr{H}\in \mathrm{V}$$