Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-reg Structured version   Visualization version   Unicode version

Definition df-reg 20344
 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.)
Assertion
Ref Expression
df-reg
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-reg
StepHypRef Expression
1 creg 20337 . 2
2 vy . . . . . . . 8
3 vz . . . . . . . 8
42, 3wel 1890 . . . . . . 7
53cv 1445 . . . . . . . . 9
6 vj . . . . . . . . . . 11
76cv 1445 . . . . . . . . . 10
8 ccl 20045 . . . . . . . . . 10
97, 8cfv 5585 . . . . . . . . 9
105, 9cfv 5585 . . . . . . . 8
11 vx . . . . . . . . 9
1211cv 1445 . . . . . . . 8
1310, 12wss 3406 . . . . . . 7
144, 13wa 371 . . . . . 6
1514, 3, 7wrex 2740 . . . . 5
1615, 2, 12wral 2739 . . . 4
1716, 11, 7wral 2739 . . 3
18 ctop 19929 . . 3
1917, 6, 18crab 2743 . 2
201, 19wceq 1446 1
 Colors of variables: wff setvar class This definition is referenced by:  isreg  20360
 Copyright terms: Public domain W3C validator