Metamath Proof Explorer


Definition df-squarenn

Description: Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion df-squarenn NN = { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csquarenn NN
1 vx 𝑥
2 cn
3 csqrt
4 1 cv 𝑥
5 4 3 cfv ( √ ‘ 𝑥 )
6 cq
7 5 6 wcel ( √ ‘ 𝑥 ) ∈ ℚ
8 7 1 2 crab { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ }
9 0 8 wceq NN = { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ }