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 𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
Assertion mpoexg ( ( 𝐴𝑅𝐵𝑆 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 mpoexg.1 𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 )
2 elex ( 𝐵𝑆𝐵 ∈ V )
3 elex ( 𝐵 ∈ V → 𝐵 ∈ V )
4 3 ralrimivw ( 𝐵 ∈ V → ∀ 𝑥𝐴 𝐵 ∈ V )
5 2 4 syl ( 𝐵𝑆 → ∀ 𝑥𝐴 𝐵 ∈ V )
6 1 mpoexxg ( ( 𝐴𝑅 ∧ ∀ 𝑥𝐴 𝐵 ∈ V ) → 𝐹 ∈ V )
7 5 6 sylan2 ( ( 𝐴𝑅𝐵𝑆 ) → 𝐹 ∈ V )