# 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 C_ F ) -> ( F |` dom G ) = G )`

### Proof

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