This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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