Metamath Proof Explorer


Theorem funssres

Description: The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994)

Ref Expression
Assertion funssres Fun F G F F dom G = G

Proof

Step Hyp Ref Expression
1 vex x V
2 vex y V
3 1 2 opeldm x y G x dom G
4 3 a1i G F x y G x dom G
5 ssel G F x y G x y F
6 4 5 jcad G F x y G x dom G x y F
7 6 adantl Fun F G F x y G x dom G x y F
8 funeu2 Fun F x y F ∃! y x y F
9 1 eldm2 x dom G y x y G
10 5 ancrd G F x y G x y F x y G
11 10 eximdv G F y x y G y x y F x y G
12 9 11 syl5bi G F x dom G y x y F x y G
13 12 imp G F x dom G y x y F x y G
14 eupick ∃! y x y F y x y F x y G x y F x y G
15 8 13 14 syl2an Fun F x y F G F x dom G x y F x y G
16 15 exp43 Fun F x y F G F x dom G x y F x y G
17 16 com23 Fun F G F x y F x dom G x y F x y G
18 17 imp Fun F G F x y F x dom G x y F x y G
19 18 com34 Fun F G F x y F x y F x dom G x y G
20 19 pm2.43d Fun F G F x y F x dom G x y G
21 20 impcomd Fun F G F x dom G x y F x y G
22 7 21 impbid Fun F G F x y G x dom G x y F
23 2 opelresi x y F dom G x dom G x y F
24 22 23 syl6rbbr Fun F G F x y F dom G x y G
25 24 alrimivv Fun F G F x y x y F dom G x y G
26 relres Rel F dom G
27 funrel Fun F Rel F
28 relss G F Rel F Rel G
29 27 28 mpan9 Fun F G F Rel G
30 eqrel Rel F dom G Rel G F dom G = G x y x y F dom G x y G
31 26 29 30 sylancr Fun F G F F dom G = G x y x y F dom G x y G
32 25 31 mpbird Fun F G F F dom G = G