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 )