Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Definition df-oexp 5348
 Description: Define the ordinal exponentiation operation.
Assertion
Ref Expression
df-oexp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-oexp
StepHypRef Expression
1 coe 5343 . 2
2 vx . . . . . . 7
32cv 1585 . . . . . 6
4 con0 3811 . . . . . 6
53, 4wcel 1588 . . . . 5
6 vy . . . . . . 7
76cv 1585 . . . . . 6
87, 4wcel 1588 . . . . 5
95, 8wa 337 . . . 4
10 vz . . . . . 6
1110cv 1585 . . . . 5
12 c0 3082 . . . . . . 7
133, 12wceq 1586 . . . . . 6
14 c1o 5339 . . . . . . 7
1514, 7cdif 2824 . . . . . 6
16 vv . . . . . . . . . . 11
1716cv 1585 . . . . . . . . . 10
18 vw . . . . . . . . . . . 12
1918cv 1585 . . . . . . . . . . 11
20 comu 5342 . . . . . . . . . . 11
2119, 3, 20co 4981 . . . . . . . . . 10
2217, 21wceq 1586 . . . . . . . . 9
2322, 18, 16copab 3565 . . . . . . . 8
2423, 14crdg 5303 . . . . . . 7
257, 24cfv 4131 . . . . . 6
2613, 15, 25cif 3180 . . . . 5
2711, 26wceq 1586 . . . 4
289, 27wa 337 . . 3
2928, 2, 6, 10copab2 4982 . 2
301, 29wceq 1586 1
 Colors of variables: wff set class This definition is referenced by:  oev 5364