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

Definition df-cpn 22100
 Description: Define the set of -times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)
Assertion
Ref Expression
df-cpn
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cpn
StepHypRef Expression
1 ccpn 22096 . 2
2 vs . . 3
3 cc 9491 . . . 4
43cpw 4010 . . 3
5 vx . . . 4
6 cn0 10796 . . . 4
75cv 1378 . . . . . . 7
82cv 1378 . . . . . . . 8
9 vf . . . . . . . . 9
109cv 1378 . . . . . . . 8
11 cdvn 22095 . . . . . . . 8
128, 10, 11co 6285 . . . . . . 7
137, 12cfv 5588 . . . . . 6
1410cdm 4999 . . . . . . 7
15 ccncf 21207 . . . . . . 7
1614, 3, 15co 6285 . . . . . 6
1713, 16wcel 1767 . . . . 5
18 cpm 7422 . . . . . 6
193, 8, 18co 6285 . . . . 5
2017, 9, 19crab 2818 . . . 4
215, 6, 20cmpt 4505 . . 3
222, 4, 21cmpt 4505 . 2
231, 22wceq 1379 1
 Colors of variables: wff setvar class This definition is referenced by:  cpnfval  22162
 Copyright terms: Public domain W3C validator