Theorem kqfval

Description: Value of the function appearing in df-kq . (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion	kqfval	|- ( ( J e. V /\ A e. X ) -> ( F ` A ) = { y e. J | A e. y } )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
2		id	|- ( A e. X -> A e. X )
3		rabexg	|- ( J e. V -> { y e. J | A e. y } e. _V )
4		eleq1	|- ( x = A -> ( x e. y <-> A e. y ) )
5	4	rabbidv	|- ( x = A -> { y e. J | x e. y } = { y e. J | A e. y } )
6	5 1	fvmptg	|- ( ( A e. X /\ { y e. J | A e. y } e. _V ) -> ( F ` A ) = { y e. J | A e. y } )
7	2 3 6	syl2anr	|- ( ( J e. V /\ A e. X ) -> ( F ` A ) = { y e. J | A e. y } )