Theorem mpoexd

Description: Existence of an operation class abstraction. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	mpoexd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	mpoexd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion	mpoexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		mpoexd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		mpoexd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
5	4	mpoexxg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
6	1 3 5	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )