Definition df-reg

Description: Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Assertion	df-reg	|- Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creg	|- Reg
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5		vy	|- y
6	3	cv	|- x
7		vz	|- z
8	5	cv	|- y
9	7	cv	|- z
10	8 9	wcel	|- y e. z
11		ccl	|- cls
12	4 11	cfv	|- ( cls ` j )
13	9 12	cfv	|- ( ( cls ` j ) ` z )
14	13 6	wss	|- ( ( cls ` j ) ` z ) C_ x
15	10 14	wa	|- ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
16	15 7 4	wrex	|- E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
17	16 5 6	wral	|- A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
18	17 3 4	wral	|- A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x )
19	18 1 2	crab	|- { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }
20	0 19	wceq	|- Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }