df-apply - Mathbox for Scott Fenton

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

Definition df-apply 31980

Description: Define the application function. See brapply 32045 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**
Step	Hyp	Ref	Expression
1		capply 31952	. 2 Apply
2		cbigcup 31941	. . . 4
3	2, 2	ccom 5118	. . 3
4		cvv 3200	. . . . . 6
5	4, 4	cxp 5112	. . . . 5
6		cep 5028	. . . . . . . 8
7	4, 6	ctxp 31937	. . . . . . 7
8		csingles 31946	. . . . . . . . 9
9	6, 8	cres 5116	. . . . . . . 8
10	9, 4	ctxp 31937	. . . . . . 7
11	7, 10	csymdif 3843	. . . . . 6 $/_\$
12	11	crn 5115	. . . . 5 $/_\$
13	5, 12	cdif 3571	. . . 4 $\$ $/_\$
14		csingle 31945	. . . . . 6 Singleton
15		cimg 31949	. . . . . 6 Img
16	14, 15	ccom 5118	. . . . 5 Singleton Img
17		cid 5023	. . . . . 6
18	17, 14	cpprod 31938	. . . . 5 pprod Singleton
19	16, 18	ccom 5118	. . . 4 Singleton Img pprod Singleton
20	13, 19	ccom 5118	. . 3 $\$ $/_\$ Singleton Img pprod Singleton
21	3, 20	ccom 5118	. 2 $\$ $/_\$ Singleton Img pprod Singleton
22	1, 21	wceq 1483	1 Apply $\$ $/_\$ Singleton Img pprod Singleton

Colors of variables: wff setvar class

This definition is referenced by: brapply 32045