HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-ni 6518
Description: Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 6758, and is intended to be used only by the construction.
Assertion
Ref Expression
df-ni |- N. = (om \ {(/)})

Detailed syntax breakdown of Definition df-ni
StepHypRef Expression
1 cnpi 6490 . 2 class N.
2 com 4085 . . 3 class om
3 c0 3082 . . . 4 class (/)
43csn 3238 . . 3 class {(/)}
52, 4cdif 2824 . 2 class (om \ {(/)})
61, 5wceq 1586 1 wff N. = (om \ {(/)})
Colors of variables: wff set class
This definition is referenced by:  elni 6522  pinn 6524  niex 6527  dmaddpi 6536  dmmulpi 6537
Copyright terms: Public domain