Theorem mpoexd

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

	Ref	Expression
Hypotheses	mpoexd.1	|- ( ph -> A e. V )
	mpoexd.2	|- ( ( ph /\ x e. A ) -> B e. W )
Assertion	mpoexd	|- ( ph -> ( x e. A , y e. B |-> C ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		mpoexd.1	|- ( ph -> A e. V )
2		mpoexd.2	|- ( ( ph /\ x e. A ) -> B e. W )
3	2	ralrimiva	|- ( ph -> A. x e. A B e. W )
4		eqid	|- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
5	4	mpoexxg	|- ( ( A e. V /\ A. x e. A B e. W ) -> ( x e. A , y e. B |-> C ) e. _V )
6	1 3 5	syl2anc	|- ( ph -> ( x e. A , y e. B |-> C ) e. _V )