Metamath Proof Explorer


Theorem fssrescdmd

Description: Restriction of a function to a subclass of its domain as a function with domain and codomain. (Contributed by AV, 13-May-2025)

Ref Expression
Hypotheses fssrescdmd.f φF:AB
fssrescdmd.c φCA
fssrescdmd.d φFCD
Assertion fssrescdmd φFC:CD

Proof

Step Hyp Ref Expression
1 fssrescdmd.f φF:AB
2 fssrescdmd.c φCA
3 fssrescdmd.d φFCD
4 1 ffnd φFFnA
5 4 2 fnssresd φFCFnC
6 resima FCC=FC
7 6 3 eqsstrid φFCCD
8 1 ffund φFunF
9 8 funresd φFunFC
10 1 fdmd φdomF=A
11 2 10 sseqtrrd φCdomF
12 ssdmres CdomFdomFC=C
13 12 a1i φCdomFdomFC=C
14 eqcom domFC=CC=domFC
15 13 14 bitrdi φCdomFC=domFC
16 11 15 mpbid φC=domFC
17 16 eqimssd φCdomFC
18 funimass4 FunFCCdomFCFCCDxCFCxD
19 9 17 18 syl2anc φFCCDxCFCxD
20 7 19 mpbid φxCFCxD
21 ffnfv FC:CDFCFnCxCFCxD
22 5 20 21 sylanbrc φFC:CD