Definition df-ce 6107

Description: Define cardinal exponentiation. Definition from [Rosser] p. 381. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-ce	|- ↑c = (n e. NC , m e. NC |-> {g | E.aE.b(~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))})

Distinct variable group:   m,n,g,a,b

Detailed syntax breakdown of Definition df-ce

Step	Hyp	Ref	Expression
1		cce 6097	. 2 class ↑c
2		vn	. . 3 setvar n
3		vm	. . 3 setvar m
4		cncs 6089	. . 3 class NC
5		va	. . . . . . . . . 10 setvar a
6	5	cv 1641	. . . . . . . . 9 class a
7	6	cpw1 4136	. . . . . . . 8 class ~P1 a
8	2	cv 1641	. . . . . . . 8 class n
9	7, 8	wcel 1710	. . . . . . 7 wff ~P1 a e. n
10		vb	. . . . . . . . . 10 setvar b
11	10	cv 1641	. . . . . . . . 9 class b
12	11	cpw1 4136	. . . . . . . 8 class ~P1 b
13	3	cv 1641	. . . . . . . 8 class m
14	12, 13	wcel 1710	. . . . . . 7 wff ~P1 b e. m
15		vg	. . . . . . . . 9 setvar g
16	15	cv 1641	. . . . . . . 8 class g
17		cmap 6000	. . . . . . . . 9 class ^m
18	6, 11, 17	co 5526	. . . . . . . 8 class (a ^m b)
19		cen 6029	. . . . . . . 8 class ~~
20	16, 18, 19	wbr 4640	. . . . . . 7 wff g ~~ (a ^m b)
21	9, 14, 20	w3a 934	. . . . . 6 wff (~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))
22	21, 10	wex 1541	. . . . 5 wff E.b(~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))
23	22, 5	wex 1541	. . . 4 wff E.aE.b(~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))
24	23, 15	cab 2339	. . 3 class {g | E.aE.b(~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))}
25	2, 3, 4, 4, 24	cmpt2 5654	. 2 class (n e. NC , m e. NC |-> {g | E.aE.b(~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))})
26	1, 25	wceq 1642	1 wff ↑c = (n e. NC , m e. NC |-> {g | E.aE.b(~P1 a e. n /\ ~P1 b e. m /\ g ~~ (a ^m b))})

This definition is referenced by:  ovce  6173  ceex  6175  fnce  6177