Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  resfunexg Unicode version

Theorem resfunexg 5382
 Description: The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.)
Assertion
Ref Expression
resfunexg

Proof of Theorem resfunexg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 funres 4941 . . . . 5
2 funfvex 5192 . . . . . 6
32ralrimiva 2392 . . . . 5
4 fnasrng 5343 . . . . 5
51, 3, 43syl 17 . . . 4
71adantr 261 . . . . 5
8 funfn 4931 . . . . 5
97, 8sylib 127 . . . 4
10 dffn5im 5219 . . . 4
119, 10syl 14 . . 3
12 imadmrn 4678 . . . . 5
13 vex 2560 . . . . . . . . 9
14 opexgOLD 3965 . . . . . . . . 9
1513, 2, 14sylancr 393 . . . . . . . 8
1615ralrimiva 2392 . . . . . . 7
17 dmmptg 4818 . . . . . . 7
181, 16, 173syl 17 . . . . . 6
1918imaeq2d 4668 . . . . 5
2012, 19syl5reqr 2087 . . . 4