This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }