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

Definition df-nrm 17386
 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 17379 . 2
2 vy . . . . . . . . 9
32cv 1652 . . . . . . . 8
4 vz . . . . . . . . 9
54cv 1652 . . . . . . . 8
63, 5wss 3322 . . . . . . 7
7 vj . . . . . . . . . . 11
87cv 1652 . . . . . . . . . 10
9 ccl 17087 . . . . . . . . . 10
108, 9cfv 5457 . . . . . . . . 9
115, 10cfv 5457 . . . . . . . 8
12 vx . . . . . . . . 9
1312cv 1652 . . . . . . . 8
1411, 13wss 3322 . . . . . . 7
156, 14wa 360 . . . . . 6
1615, 4, 8wrex 2708 . . . . 5
17 ccld 17085 . . . . . . 7
188, 17cfv 5457 . . . . . 6
1913cpw 3801 . . . . . 6
2018, 19cin 3321 . . . . 5
2116, 2, 20wral 2707 . . . 4
2221, 12, 8wral 2707 . . 3
23 ctop 16963 . . 3
2422, 7, 23crab 2711 . 2
251, 24wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isnrm  17404
 Copyright terms: Public domain W3C validator