Metamath Proof Explorer


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 abbi2i ℕ = { 𝑥 ∣ ( 𝑥 ∈ ℤ ∧ 1 ≤ 𝑥 ) }
3 df-rab { 𝑥 ∈ ℤ ∣ 1 ≤ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ℤ ∧ 1 ≤ 𝑥 ) }
4 2 3 eqtr4i ℕ = { 𝑥 ∈ ℤ ∣ 1 ≤ 𝑥 }