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

Definition df-cncf 18900
 Description: Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
Assertion
Ref Expression
df-cncf
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-cncf
StepHypRef Expression
1 ccncf 18898 . 2
2 va . . 3
3 vb . . 3
4 cc 8980 . . . 4
54cpw 3791 . . 3
6 vx . . . . . . . . . . . . 13
76cv 1651 . . . . . . . . . . . 12
8 vy . . . . . . . . . . . . 13
98cv 1651 . . . . . . . . . . . 12
10 cmin 9283 . . . . . . . . . . . 12
117, 9, 10co 6073 . . . . . . . . . . 11
12 cabs 12031 . . . . . . . . . . 11
1311, 12cfv 5446 . . . . . . . . . 10
14 vd . . . . . . . . . . 11
1514cv 1651 . . . . . . . . . 10
16 clt 9112 . . . . . . . . . 10
1713, 15, 16wbr 4204 . . . . . . . . 9
18 vf . . . . . . . . . . . . . 14
1918cv 1651 . . . . . . . . . . . . 13
207, 19cfv 5446 . . . . . . . . . . . 12
219, 19cfv 5446 . . . . . . . . . . . 12
2220, 21, 10co 6073 . . . . . . . . . . 11
2322, 12cfv 5446 . . . . . . . . . 10
24 ve . . . . . . . . . . 11
2524cv 1651 . . . . . . . . . 10
2623, 25, 16wbr 4204 . . . . . . . . 9
2717, 26wi 4 . . . . . . . 8
282cv 1651 . . . . . . . 8
2927, 8, 28wral 2697 . . . . . . 7
30 crp 10604 . . . . . . 7
3129, 14, 30wrex 2698 . . . . . 6
3231, 24, 30wral 2697 . . . . 5
3332, 6, 28wral 2697 . . . 4
343cv 1651 . . . . 5
35 cmap 7010 . . . . 5
3634, 28, 35co 6073 . . . 4
3733, 18, 36crab 2701 . . 3
382, 3, 5, 5, 37cmpt2 6075 . 2
391, 38wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  cncfval  18910  cncfrss  18913  cncfrss2  18914
 Copyright terms: Public domain W3C validator