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

Definition df-rest 14353
Description: Function returning the subspace topology induced by the topology and the set . (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
Assertion
Ref Expression
df-rest
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-rest
StepHypRef Expression
1 crest 14351 . 2
2 vj . . 3
3 vx . . 3
4 cvv 2967 . . 3
5 vy . . . . 5
62cv 1368 . . . . 5
75cv 1368 . . . . . 6
83cv 1368 . . . . . 6
97, 8cin 3322 . . . . 5
105, 6, 9cmpt 4345 . . . 4
1110crn 4836 . . 3
122, 3, 4, 4, 11cmpt2 6088 . 2
131, 12wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  restfn  14355  restval  14357
  Copyright terms: Public domain W3C validator