0xnn0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 0xnn0		Structured version Visualization version GIF version

Theorem 0xnn0 12678

Description: Zero is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020.)

**Assertion**
Ref	Expression
0xnn0	⊢ 0 ∈ ℕ₀^*

**Proof of Theorem 0xnn0**
Step	Hyp	Ref	Expression
1		nn0ssxnn0 12675	. 2 ⊢ ℕ₀ ⊆ ℕ₀^*
2		0nn0 12614	. 2 ⊢ 0 ∈ ℕ₀
3	1, 2	sselii 3928	1 ⊢ 0 ∈ ℕ₀^*

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2145 0cc0 11193 ℕ₀cn0 12599 ℕ₀^*cxnn0 12672

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2733 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-mulcl 11255 ax-i2m1 11261

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2740 df-cleq 2753 df-clel 2836 df-v 3453 df-un 3904 df-ss 3916 df-sn 4585 df-n0 12600 df-xnn0 12673

This theorem is used by: 0edg0rgr 30146 rgrusgrprc 30163 rusgrprc 30164 rgrprcx 30166