Metamath Proof Explorer


Theorem fnresdmss

Description: A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion fnresdmss FFnAABFB=F

Proof

Step Hyp Ref Expression
1 fnrel FFnARelF
2 fndm FFnAdomF=A
3 2 adantr FFnAABdomF=A
4 simpr FFnAABAB
5 3 4 eqsstrd FFnAABdomFB
6 relssres RelFdomFBFB=F
7 1 5 6 syl2an2r FFnAABFB=F