Metamath Proof Explorer


Theorem axcnex

Description: The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT ), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep in later theorems by invoking Axiom ax-cnex instead of cnexALT . Use cnex instead. (Contributed by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Assertion axcnex ℂ ∈ V

Proof

Step Hyp Ref Expression
1 df-c ℂ = ( R × R )
2 nrex1 R ∈ V
3 2 2 xpex ( R × R ) ∈ V
4 1 3 eqeltri ℂ ∈ V