Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cur1vald Unicode version

Theorem cur1vald 25302
 Description: The value of a curried operation. (Contributed by FL, 17-May-2010.)
Assertion
Ref Expression
cur1vald
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem cur1vald
StepHypRef Expression
1 simp1 955 . . . . . . 7
2 xpexg 4816 . . . . . . . 8
323adant1 973 . . . . . . 7
4 fnex 5757 . . . . . . 7
51, 3, 4syl2anc 642 . . . . . 6
653expib 1154 . . . . 5
76adantr 451 . . . 4
87imp 418 . . 3
9 fnfun 5357 . . . 4
11 fndm 5359 . . . . 5
12 relxp 4810 . . . . . 6
13 releq 4787 . . . . . . 7
1413eqcoms 2299 . . . . . 6
1512, 14mpbii 202 . . . . 5
1611, 15syl 15 . . . 4
18 cur1val 25301 . . 3
198, 10, 17, 18syl3anc 1182 . 2
2011dmeqd 4897 . . . . . 6
21 dmxp 4913 . . . . . . . . 9
2221eqeq1d 2304 . . . . . . . 8
2322biimpcd 215 . . . . . . 7
2423eqcoms 2299 . . . . . 6
2520, 24syl 15 . . . . 5
2625imp 418 . . . 4