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 = { 𝑥 ∈ ℕ ∣ ( √ ‘ 𝑥 ) ∈ ℚ }