Metamath Proof Explorer


Theorem 1n0OLD

Description: Obsolete version of 1n0 as of 10-Jun-2026. (Contributed by NM, 26-Dec-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 1n0OLD 1 𝑜

Proof

Step Hyp Ref Expression
1 df1o2 1 𝑜 =
2 0ex V
3 2 snnz
4 1 3 eqnetri 1 𝑜