# 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 ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to {{F}↾}_{\mathrm{dom}{G}}={G}$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 vex ${⊢}{y}\in \mathrm{V}$
3 1 2 opeldm ${⊢}⟨{x},{y}⟩\in {G}\to {x}\in \mathrm{dom}{G}$
4 3 a1i ${⊢}{G}\subseteq {F}\to \left(⟨{x},{y}⟩\in {G}\to {x}\in \mathrm{dom}{G}\right)$
5 ssel ${⊢}{G}\subseteq {F}\to \left(⟨{x},{y}⟩\in {G}\to ⟨{x},{y}⟩\in {F}\right)$
6 4 5 jcad ${⊢}{G}\subseteq {F}\to \left(⟨{x},{y}⟩\in {G}\to \left({x}\in \mathrm{dom}{G}\wedge ⟨{x},{y}⟩\in {F}\right)\right)$
7 6 adantl ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(⟨{x},{y}⟩\in {G}\to \left({x}\in \mathrm{dom}{G}\wedge ⟨{x},{y}⟩\in {F}\right)\right)$
8 funeu2 ${⊢}\left(\mathrm{Fun}{F}\wedge ⟨{x},{y}⟩\in {F}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {F}$
9 1 eldm2 ${⊢}{x}\in \mathrm{dom}{G}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {G}$
10 5 ancrd ${⊢}{G}\subseteq {F}\to \left(⟨{x},{y}⟩\in {G}\to \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{y}⟩\in {G}\right)\right)$
11 10 eximdv ${⊢}{G}\subseteq {F}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {G}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{y}⟩\in {G}\right)\right)$
12 9 11 syl5bi ${⊢}{G}\subseteq {F}\to \left({x}\in \mathrm{dom}{G}\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{y}⟩\in {G}\right)\right)$
13 12 imp ${⊢}\left({G}\subseteq {F}\wedge {x}\in \mathrm{dom}{G}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{y}⟩\in {G}\right)$
14 eupick ${⊢}\left(\exists !{y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {F}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{y}⟩\in {G}\right)\right)\to \left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in {G}\right)$
15 8 13 14 syl2an ${⊢}\left(\left(\mathrm{Fun}{F}\wedge ⟨{x},{y}⟩\in {F}\right)\wedge \left({G}\subseteq {F}\wedge {x}\in \mathrm{dom}{G}\right)\right)\to \left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in {G}\right)$
16 15 exp43 ${⊢}\mathrm{Fun}{F}\to \left(⟨{x},{y}⟩\in {F}\to \left({G}\subseteq {F}\to \left({x}\in \mathrm{dom}{G}\to \left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in {G}\right)\right)\right)\right)$
17 16 com23 ${⊢}\mathrm{Fun}{F}\to \left({G}\subseteq {F}\to \left(⟨{x},{y}⟩\in {F}\to \left({x}\in \mathrm{dom}{G}\to \left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in {G}\right)\right)\right)\right)$
18 17 imp ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(⟨{x},{y}⟩\in {F}\to \left({x}\in \mathrm{dom}{G}\to \left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in {G}\right)\right)\right)$
19 18 com34 ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(⟨{x},{y}⟩\in {F}\to \left(⟨{x},{y}⟩\in {F}\to \left({x}\in \mathrm{dom}{G}\to ⟨{x},{y}⟩\in {G}\right)\right)\right)$
20 19 pm2.43d ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(⟨{x},{y}⟩\in {F}\to \left({x}\in \mathrm{dom}{G}\to ⟨{x},{y}⟩\in {G}\right)\right)$
21 20 impcomd ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(\left({x}\in \mathrm{dom}{G}\wedge ⟨{x},{y}⟩\in {F}\right)\to ⟨{x},{y}⟩\in {G}\right)$
22 7 21 impbid ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(⟨{x},{y}⟩\in {G}↔\left({x}\in \mathrm{dom}{G}\wedge ⟨{x},{y}⟩\in {F}\right)\right)$
23 2 opelresi ${⊢}⟨{x},{y}⟩\in \left({{F}↾}_{\mathrm{dom}{G}}\right)↔\left({x}\in \mathrm{dom}{G}\wedge ⟨{x},{y}⟩\in {F}\right)$
24 22 23 syl6rbbr ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left(⟨{x},{y}⟩\in \left({{F}↾}_{\mathrm{dom}{G}}\right)↔⟨{x},{y}⟩\in {G}\right)$
25 24 alrimivv ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \left({{F}↾}_{\mathrm{dom}{G}}\right)↔⟨{x},{y}⟩\in {G}\right)$
26 relres ${⊢}\mathrm{Rel}\left({{F}↾}_{\mathrm{dom}{G}}\right)$
27 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
28 relss ${⊢}{G}\subseteq {F}\to \left(\mathrm{Rel}{F}\to \mathrm{Rel}{G}\right)$
29 27 28 mpan9 ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \mathrm{Rel}{G}$
30 eqrel ${⊢}\left(\mathrm{Rel}\left({{F}↾}_{\mathrm{dom}{G}}\right)\wedge \mathrm{Rel}{G}\right)\to \left({{F}↾}_{\mathrm{dom}{G}}={G}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \left({{F}↾}_{\mathrm{dom}{G}}\right)↔⟨{x},{y}⟩\in {G}\right)\right)$
31 26 29 30 sylancr ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to \left({{F}↾}_{\mathrm{dom}{G}}={G}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in \left({{F}↾}_{\mathrm{dom}{G}}\right)↔⟨{x},{y}⟩\in {G}\right)\right)$
32 25 31 mpbird ${⊢}\left(\mathrm{Fun}{F}\wedge {G}\subseteq {F}\right)\to {{F}↾}_{\mathrm{dom}{G}}={G}$