Theorem elfvmptrab

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

	Ref	Expression
Hypotheses	elfvmptrab.f	|- F = ( x e. V |-> { y e. M | ph } )
	elfvmptrab.v	|- ( X e. V -> M e. _V )
Assertion	elfvmptrab	|- ( Y e. ( F ` X ) -> ( X e. V /\ Y e. M ) )

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab.f	|- F = ( x e. V |-> { y e. M | ph } )
2		elfvmptrab.v	|- ( X e. V -> M e. _V )
3		csbconstg	|- ( x e. V -> [_ x / m ]_ M = M )
4	3	eqcomd	|- ( x e. V -> M = [_ x / m ]_ M )
5		rabeq	|- ( M = [_ x / m ]_ M -> { y e. M | ph } = { y e. [_ x / m ]_ M | ph } )
6	4 5	syl	|- ( x e. V -> { y e. M | ph } = { y e. [_ x / m ]_ M | ph } )
7	6	mpteq2ia	|- ( x e. V |-> { y e. M | ph } ) = ( x e. V |-> { y e. [_ x / m ]_ M | ph } )
8	1 7	eqtri	|- F = ( x e. V |-> { y e. [_ x / m ]_ M | ph } )
9		csbconstg	|- ( X e. V -> [_ X / m ]_ M = M )
10	9 2	eqeltrd	|- ( X e. V -> [_ X / m ]_ M e. _V )
11	8 10	elfvmptrab1w	|- ( Y e. ( F ` X ) -> ( X e. V /\ Y e. [_ X / m ]_ M ) )
12	9	eleq2d	|- ( X e. V -> ( Y e. [_ X / m ]_ M <-> Y e. M ) )
13	12	biimpd	|- ( X e. V -> ( Y e. [_ X / m ]_ M -> Y e. M ) )
14	13	imdistani	|- ( ( X e. V /\ Y e. [_ X / m ]_ M ) -> ( X e. V /\ Y e. M ) )
15	11 14	syl	|- ( Y e. ( F ` X ) -> ( X e. V /\ Y e. M ) )