Axiom ax-cnex

Description: The complex numbers form a set. This axiom is redundant - see cnexALT - but we provide this axiom because the justification theorem axcnex does not use ax-rep even though the redundancy proof does. Proofs should normally use cnex instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995)

	Ref	Expression
Assertion	ax-cnex	$$⊢ℂ\in \mathrm{V}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cc	$$classℂ$$
1		cvv	$$class\mathrm{V}$$
2	0 1	wcel	$$wffℂ\in \mathrm{V}$$