ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-0id Unicode version

Axiom ax-0id 6791
Description:  0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6762.

Proofs should normally use addid1 6948 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

Assertion
Ref Expression
ax-0id  CC  +  0

Detailed syntax breakdown of Axiom ax-0id
StepHypRef Expression
1 cA . . 3
2 cc 6709 . . 3  CC
31, 2wcel 1390 . 2  CC
4 cc0 6711 . . . 4  0
5 caddc 6714 . . . 4  +
61, 4, 5co 5455 . . 3  +  0
76, 1wceq 1242 . 2  +  0
83, 7wi 4 1  CC  +  0
Colors of variables: wff set class
This axiom is referenced by:  addid1  6948
  Copyright terms: Public domain W3C validator