Theorem resmpti

Description: Restriction of the mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	resmpti.1	|- B C_ A
Assertion	resmpti	|- ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C )

Proof

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