Theorem resmpt

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		resopab2	|- ( B C_ A -> ( { <. x , y >. | ( x e. A /\ y = C ) } |` B ) = { <. x , y >. | ( x e. B /\ y = C ) } )
2		df-mpt	|- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
3	2	reseq1i	|- ( ( x e. A |-> C ) |` B ) = ( { <. x , y >. | ( x e. A /\ y = C ) } |` B )
4		df-mpt	|- ( x e. B |-> C ) = { <. x , y >. | ( x e. B /\ y = C ) }
5	1 3 4	3eqtr4g	|- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )