Metamath Proof Explorer

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 \in A, y \in B ⟼ C)$
	Assertion	mpoexg	$⊢ (A \in R \land B \in S) \to F \in V$

Step	Hyp	Ref	Expression
1		mpoexg.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		elex	$⊢ B \in S \to B \in V$
3		elex	$⊢ B \in V \to B \in V$
4	3	ralrimivw	$⊢ B \in V \to \forall x \in A B \in V$
5	2 4	syl	$⊢ B \in S \to \forall x \in A B \in V$
6	1	mpoexxg	$⊢ (A \in R \land \forall x \in A B \in V) \to F \in V$
7	5 6	sylan2	$⊢ (A \in R \land B \in S) \to F \in V$