Metamath Proof Explorer


Theorem dfn2

Description: The set of positive integers defined in terms of nonnegative integers. (Contributed by NM, 23-Sep-2007) (Proof shortened by Mario Carneiro, 13-Feb-2013)

Ref Expression
Assertion dfn2 = 0 0

Proof

Step Hyp Ref Expression
1 df-n0 0 = 0
2 1 difeq1i 0 0 = 0 0
3 difun2 0 0 = 0
4 0nnn ¬ 0
5 difsn ¬ 0 0 =
6 4 5 ax-mp 0 =
7 2 3 6 3eqtrri = 0 0