Axiom ax-addcl

Description: Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by Theorem axaddcl . Proofs should normally use addcl instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

	Ref	Expression
Assertion	ax-addcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B\in ℂ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cc	$$classℂ$$
2	0 1	wcel	$$wffA\in ℂ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℂ$$
5	2 4	wa	$$wff\left(A\in ℂ\wedge B\in ℂ\right)$$
6		caddc	$$class+$$
7	0 3 6	co	$$class\left(A+B\right)$$
8	7 1	wcel	$$wffA+B\in ℂ$$
9	5 8	wi	$$wff\left(\left(A\in ℂ\wedge B\in ℂ\right)\to A+B\in ℂ\right)$$