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 = { x e. NN | ( sqrt ` x ) e. QQ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csquarenn	|- []NN
1		vx	|- x
2		cn	|- NN
3		csqrt	|- sqrt
4	1	cv	|- x
5	4 3	cfv	|- ( sqrt ` x )
6		cq	|- QQ
7	5 6	wcel	|- ( sqrt ` x ) e. QQ
8	7 1 2	crab	|- { x e. NN | ( sqrt ` x ) e. QQ }
9	0 8	wceq	|- []NN = { x e. NN | ( sqrt ` x ) e. QQ }