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

Definition df-nrm 20113
 Description: Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)
Assertion
Ref Expression
df-nrm
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-nrm
StepHypRef Expression
1 cnrm 20106 . 2
2 vy . . . . . . . . 9
32cv 1406 . . . . . . . 8
4 vz . . . . . . . . 9
54cv 1406 . . . . . . . 8
63, 5wss 3416 . . . . . . 7
7 vj . . . . . . . . . . 11
87cv 1406 . . . . . . . . . 10
9 ccl 19813 . . . . . . . . . 10
108, 9cfv 5571 . . . . . . . . 9
115, 10cfv 5571 . . . . . . . 8
12 vx . . . . . . . . 9
1312cv 1406 . . . . . . . 8
1411, 13wss 3416 . . . . . . 7
156, 14wa 369 . . . . . 6
1615, 4, 8wrex 2757 . . . . 5
17 ccld 19811 . . . . . . 7
188, 17cfv 5571 . . . . . 6
1913cpw 3957 . . . . . 6
2018, 19cin 3415 . . . . 5
2116, 2, 20wral 2756 . . . 4
2221, 12, 8wral 2756 . . 3
23 ctop 19688 . . 3
2422, 7, 23crab 2760 . 2
251, 24wceq 1407 1
 Colors of variables: wff setvar class This definition is referenced by:  isnrm  20131
 Copyright terms: Public domain W3C validator