Definition df-squarenn

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

	Ref	Expression
Assertion	df-squarenn	$$⊢{◻}_{\mathbb{N}}=\left\{x\in \mathbb{N}|\sqrt{x}\in \mathbb{Q}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csquarenn	$$class{◻}_{\mathbb{N}}$$
1		vx	$$setvarx$$
2		cn	$$class\mathbb{N}$$
3		csqrt	$$class\surd$$
4	1	cv	$$setvarx$$
5	4 3	cfv	$$class\sqrt{x}$$
6		cq	$$class\mathbb{Q}$$
7	5 6	wcel	$$wff\sqrt{x}\in \mathbb{Q}$$
8	7 1 2	crab	$$class\left\{x\in \mathbb{N}|\sqrt{x}\in \mathbb{Q}\right\}$$
9	0 8	wceq	$$wff{◻}_{\mathbb{N}}=\left\{x\in \mathbb{N}|\sqrt{x}\in \mathbb{Q}\right\}$$