Theorem fvmptrabfv

Description: Value of a function mapping a set to a class abstraction restricting the value of another function. (Contributed by AV, 18-Feb-2022)

	Ref	Expression
Hypotheses	fvmptrabfv.f	|- F = ( x e. _V |-> { y e. ( G ` x ) | ph } )
	fvmptrabfv.r	|- ( x = X -> ( ph <-> ps ) )
Assertion	fvmptrabfv	|- ( F ` X ) = { y e. ( G ` X ) | ps }

Proof

Step	Hyp	Ref	Expression
1		fvmptrabfv.f	|- F = ( x e. _V |-> { y e. ( G ` x ) | ph } )
2		fvmptrabfv.r	|- ( x = X -> ( ph <-> ps ) )
3		fveq2	|- ( x = X -> ( G ` x ) = ( G ` X ) )
4	3 2	rabeqbidv	|- ( x = X -> { y e. ( G ` x ) | ph } = { y e. ( G ` X ) | ps } )
5		fvex	|- ( G ` X ) e. _V
6	5	rabex	|- { y e. ( G ` X ) | ps } e. _V
7	4 1 6	fvmpt	|- ( X e. _V -> ( F ` X ) = { y e. ( G ` X ) | ps } )
8		fvprc	|- ( -. X e. _V -> ( F ` X ) = (/) )
9		fvprc	|- ( -. X e. _V -> ( G ` X ) = (/) )
10	9	rabeqdv	|- ( -. X e. _V -> { y e. ( G ` X ) | ps } = { y e. (/) | ps } )
11		rab0	|- { y e. (/) | ps } = (/)
12	10 11	eqtr2di	|- ( -. X e. _V -> (/) = { y e. ( G ` X ) | ps } )
13	8 12	eqtrd	|- ( -. X e. _V -> ( F ` X ) = { y e. ( G ` X ) | ps } )
14	7 13	pm2.61i	|- ( F ` X ) = { y e. ( G ` X ) | ps }