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

Metamath Proof Explorer

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 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cc class ℂ
2 0 1 wcel wff A ∈ ℂ
3 cB class B
4 3 1 wcel wff B ∈ ℂ
5 2 4 wa wff A ∈ ℂ ∧ B ∈ ℂ
6 caddc class +
7 0 3 6 co class A + B
8 7 1 wcel wff A + B ∈ ℂ
9 5 8 wi wff A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ