Theorem nn0zrab

Description: Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004)

	Ref	Expression
Assertion	nn0zrab	⊢ ℕ0 = { 𝑥 ∈ ℤ ∣ 0 ≤ 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		elnn0z	⊢ ( 𝑥 ∈ ℕ0 ↔ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) )
2	1	eqabi	⊢ ℕ0 = { 𝑥 ∣ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) }
3		df-rab	⊢ { 𝑥 ∈ ℤ ∣ 0 ≤ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥 ) }
4	2 3	eqtr4i	⊢ ℕ0 = { 𝑥 ∈ ℤ ∣ 0 ≤ 𝑥 }