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	|- CC e. _V

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cc	|- CC
1		cvv	|- _V
2	0 1	wcel	|- CC e. _V