Theorem elovmpt3rab

Description: Implications for the value of an operation defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by AV, 17-Jul-2018) (Revised by AV, 16-May-2019)

	Ref	Expression
Hypothesis	elovmpt3rab.o	|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
Assertion	elovmpt3rab	|- ( ( M e. U /\ N e. T ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. M /\ A e. N ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpt3rab.o	|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )
2		eqidd	|- ( ( x = X /\ y = Y ) -> M = M )
3		eqidd	|- ( ( x = X /\ y = Y ) -> N = N )
4	1 2 3	elovmpt3rab1	|- ( ( M e. U /\ N e. T ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. M /\ A e. N ) ) ) )