NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ce Unicode version

Definition df-ce 6106
Description: Define cardinal exponentiation. Definition from [Rosser] p. 381. (Contributed by Scott Fenton, 24-Feb-2015.)
Assertion
Ref Expression
df-ce c NC NC 1 1
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ce
StepHypRef Expression
1 cce 6096 . 2 c
2 vn . . 3
3 vm . . 3
4 cncs 6088 . . 3 NC
5 va . . . . . . . . . 10
65cv 1641 . . . . . . . . 9
76cpw1 4135 . . . . . . . 8 1
82cv 1641 . . . . . . . 8
97, 8wcel 1710 . . . . . . 7 1
10 vb . . . . . . . . . 10
1110cv 1641 . . . . . . . . 9
1211cpw1 4135 . . . . . . . 8 1
133cv 1641 . . . . . . . 8
1412, 13wcel 1710 . . . . . . 7 1
15 vg . . . . . . . . 9
1615cv 1641 . . . . . . . 8
17 cmap 5999 . . . . . . . . 9
186, 11, 17co 5525 . . . . . . . 8
19 cen 6028 . . . . . . . 8
2016, 18, 19wbr 4639 . . . . . . 7
219, 14, 20w3a 934 . . . . . 6 1 1
2221, 10wex 1541 . . . . 5 1 1
2322, 5wex 1541 . . . 4 1 1
2423, 15cab 2339 . . 3 1 1
252, 3, 4, 4, 24cmpt2 5653 . 2 NC NC 1 1
261, 25wceq 1642 1 c NC NC 1 1
Colors of variables: wff setvar class
This definition is referenced by:  ovce  6172  ceex  6174  fnce  6176
  Copyright terms: Public domain W3C validator