Definition df-cnrm

Description: Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	df-cnrm	|- CNrm = { j e. Top | A. x e. ~P U. j ( j |`t x ) e. Nrm }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnrm	|- CNrm
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6	5	cpw	|- ~P U. j
7		crest	|- |`t
8	3	cv	|- x
9	4 8 7	co	|- ( j |`t x )
10		cnrm	|- Nrm
11	9 10	wcel	|- ( j |`t x ) e. Nrm
12	11 3 6	wral	|- A. x e. ~P U. j ( j |`t x ) e. Nrm
13	12 1 2	crab	|- { j e. Top | A. x e. ~P U. j ( j |`t x ) e. Nrm }
14	0 13	wceq	|- CNrm = { j e. Top | A. x e. ~P U. j ( j |`t x ) e. Nrm }