Theorem mpoexg

Description: Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypothesis	mpoexg.1	|- F = ( x e. A , y e. B |-> C )
Assertion	mpoexg	|- ( ( A e. R /\ B e. S ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		mpoexg.1	|- F = ( x e. A , y e. B |-> C )
2		elex	|- ( B e. S -> B e. _V )
3		elex	|- ( B e. _V -> B e. _V )
4	3	ralrimivw	|- ( B e. _V -> A. x e. A B e. _V )
5	2 4	syl	|- ( B e. S -> A. x e. A B e. _V )
6	1	mpoexxg	|- ( ( A e. R /\ A. x e. A B e. _V ) -> F e. _V )
7	5 6	sylan2	|- ( ( A e. R /\ B e. S ) -> F e. _V )