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

Definition df-reg 17382
 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 17375 . 2
2 vy . . . . . . . 8
3 vz . . . . . . . 8
42, 3wel 1727 . . . . . . 7
53cv 1652 . . . . . . . . 9
6 vj . . . . . . . . . . 11
76cv 1652 . . . . . . . . . 10
8 ccl 17084 . . . . . . . . . 10
97, 8cfv 5456 . . . . . . . . 9
105, 9cfv 5456 . . . . . . . 8
11 vx . . . . . . . . 9
1211cv 1652 . . . . . . . 8
1310, 12wss 3322 . . . . . . 7
144, 13wa 360 . . . . . 6
1514, 3, 7wrex 2708 . . . . 5
1615, 2, 12wral 2707 . . . 4
1716, 11, 7wral 2707 . . 3
18 ctop 16960 . . 3
1917, 6, 18crab 2711 . 2
201, 19wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isreg  17398
 Copyright terms: Public domain W3C validator