NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ce GIF 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 = (n NC , m NC {g ab(1a n 1b m g ≈ (am b))})
Distinct variable group:   m,n,g,a,b

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