Definition df-cnrm 21122

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

Assertion

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

Distinct variable group:   x, j

Detailed syntax breakdown of Definition df-cnrm

Step	Hyp	Ref	Expression
1		ccnrm 21115	. 2 class CNrm
2		vj	. . . . . . 7 setvar j
3	2	cv 1482	. . . . . 6 class j
4		vx	. . . . . . 7 setvar x
5	4	cv 1482	. . . . . 6 class x
6		crest 16081	. . . . . 6 class ↾t
7	3, 5, 6	co 6650	. . . . 5 class ( j ↾t x )
8		cnrm 21114	. . . . 5 class Nrm
9	7, 8	wcel 1990	. . . 4 wff ( j ↾t x ) e. Nrm
10	3	cuni 4436	. . . . 5 class U. j
11	10	cpw 4158	. . . 4 class ~P U. j
12	9, 4, 11	wral 2912	. . 3 wff A. x e. ~P U. j ( j ↾t x ) e. Nrm
13		ctop 20698	. . 3 class Top
14	12, 2, 13	crab 2916	. 2 class { j e. Top | A. x e. ~P U. j ( j ↾t x ) e. Nrm }
15	1, 14	wceq 1483	1 wff CNrm = { j e. Top | A. x e. ~P U. j ( j ↾t x ) e. Nrm }

This definition is referenced by:  iscnrm  21127