Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-apply Structured version   Unicode version

Definition df-apply 25717
 Description: Define the application function. See brapply 25783 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
Assertion
Ref Expression
df-apply Apply (++) Singleton Img pprod Singleton

Detailed syntax breakdown of Definition df-apply
StepHypRef Expression
1 capply 25689 . 2 Apply
2 cbigcup 25678 . . . 4
32, 2ccom 4882 . . 3
4 cvv 2956 . . . . . 6
54, 4cxp 4876 . . . . 5
6 cep 4492 . . . . . . . 8
74, 6ctxp 25674 . . . . . . 7
8 csingles 25683 . . . . . . . . 9
96, 8cres 4880 . . . . . . . 8
109, 4ctxp 25674 . . . . . . 7
117, 10csymdif 25662 . . . . . 6 (++)
1211crn 4879 . . . . 5 (++)
135, 12cdif 3317 . . . 4 (++)
14 csingle 25682 . . . . . 6 Singleton
15 cimg 25686 . . . . . 6 Img
1614, 15ccom 4882 . . . . 5 Singleton Img
17 cid 4493 . . . . . 6
1817, 14cpprod 25675 . . . . 5 pprod Singleton
1916, 18ccom 4882 . . . 4 Singleton Img pprod Singleton
2013, 19ccom 4882 . . 3 (++) Singleton Img pprod Singleton
213, 20ccom 4882 . 2 (++) Singleton Img pprod Singleton
221, 21wceq 1652 1 Apply (++) Singleton Img pprod Singleton
 Colors of variables: wff set class This definition is referenced by:  brapply  25783
 Copyright terms: Public domain W3C validator