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 ∈ A , y ∈ B ⟼ C
Assertion mpoexg ⊢ A ∈ R ∧ B ∈ S → F ∈ V

Proof

Step Hyp Ref Expression
1 mpoexg.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 elex ⊢ B ∈ S → B ∈ V
3 elex ⊢ B ∈ V → B ∈ V
4 3 ralrimivw ⊢ B ∈ V → ∀ x ∈ A B ∈ V
5 2 4 syl ⊢ B ∈ S → ∀ x ∈ A B ∈ V
6 1 mpoexxg ⊢ A ∈ R ∧ ∀ x ∈ A B ∈ V → F ∈ V
7 5 6 sylan2 ⊢ A ∈ R ∧ B ∈ S → F ∈ V