Theorem nnzrab

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

	Ref	Expression
Assertion	nnzrab	⊢ ℕ = { 𝑥 ∈ ℤ ∣ 1 ≤ 𝑥 }

Proof

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