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

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	$⊢ ℂ \in V$

Proof

Step	Hyp	Ref	Expression
1		df-c	$⊢ ℂ = 𝑹 \times 𝑹$
2		nrex1	$⊢ 𝑹 \in V$
3	2 2	xpex	$⊢ 𝑹 \times 𝑹 \in V$
4	1 3	eqeltri	$⊢ ℂ \in V$