HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvaddid Unicode version

Axiom ax-hvaddid 23016
Description: Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvaddid

Detailed syntax breakdown of Axiom ax-hvaddid
StepHypRef Expression
1 cA . . 3
2 chil 22931 . . 3
31, 2wcel 1724 . 2
4 c0v 22936 . . . 4
5 cva 22932 . . . 4
61, 4, 5co 6067 . . 3
76, 1wceq 1662 . 2
83, 7wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  23035  hvpncan  23051  hvsubeq0i  23075  hvsubcan2i  23076  hvsubaddi  23078  hvsub0  23088  hvaddsub4  23090  norm3difi  23159  shsel1  23334  shunssi  23381  omlsilem  23415  pjoc1i  23444  pjchi  23445  spansncvi  23665  5oalem1  23667  5oalem2  23668  3oalem2  23676  pjssmii  23694  hoaddid1i  23800  lnop0  23980  lnopmul  23981  lnfn0i  24056  lnfnmuli  24058  pjclem4  24213  pj3si  24221  hst1h  24241  sumdmdlem  24432
  Copyright terms: Public domain W3C validator