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

Definition df-ni 4972
Description: Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 5212, 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 4944 . 2 class N.
2 com 3121 . . 3 class om
3 c0 2270 . . . 4 class (/)
43csn 2399 . . 3 class {(/)}
52, 4cdif 2034 . 2 class (om \ {(/)})
61, 5wceq 953 1 wff N. = (om \ {(/)})
Colors of variables: wff set class
This definition is referenced by:  elni 4976  pinn 4978  niex 4981  dmaddpi 4990  dmmulpi 4991
Copyright terms: Public domain