Metamath Proof Explorer

Theorem mptss

Description: Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion mptss 
|- ( A C_ B -> ( x e. A |-> C ) C_ ( x e. B |-> C ) )

Proof

Step Hyp Ref Expression
1 resmpt 
 |-  ( A C_ B -> ( ( x e. B |-> C ) |` A ) = ( x e. A |-> C ) )
2 resss 
 |-  ( ( x e. B |-> C ) |` A ) C_ ( x e. B |-> C )
3 1 2 eqsstrrdi 
 |-  ( A C_ B -> ( x e. A |-> C ) C_ ( x e. B |-> C ) )