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

Metamath Proof Explorer

Axiom ax-addrcl

Description: Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by Theorem axaddrcl . Proofs should normally use readdcl instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

		Ref	Expression
	Assertion	ax-addrcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cr	$class ℝ$
2	0 1	wcel	$wff A \in ℝ$
3		cB	$class B$
4	3 1	wcel	$wff B \in ℝ$
5	2 4	wa	$wff (A \in ℝ \land B \in ℝ)$
6		caddc	$class +$
7	0 3 6	co	$class (A + B)$
8	7 1	wcel	$wff A + B \in ℝ$
9	5 8	wi	$wff ((A \in ℝ \land B \in ℝ) \to A + B \in ℝ)$