Theorem mpoexwd

Description: Deduction version of mpoexw . (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Hypotheses	mpoexwd.1	|- A e. _V
	mpoexwd.2	|- B e. _V
	mpoexwd.3	|- D e. _V
	mpoexwd.4	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
Assertion	mpoexwd	|- ( ph -> ( x e. A , y e. B |-> C ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		mpoexwd.1	|- A e. _V
2		mpoexwd.2	|- B e. _V
3		mpoexwd.3	|- D e. _V
4		mpoexwd.4	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
5		eqid	|- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
6	5	mpofun	|- Fun ( x e. A , y e. B |-> C )
7	4	ralrimivva	|- ( ph -> A. x e. A A. y e. B C e. D )
8	5	dmmpoga	|- ( A. x e. A A. y e. B C e. D -> dom ( x e. A , y e. B |-> C ) = ( A X. B ) )
9	7 8	syl	|- ( ph -> dom ( x e. A , y e. B |-> C ) = ( A X. B ) )
10	1 2	xpex	|- ( A X. B ) e. _V
11	9 10	eqeltrdi	|- ( ph -> dom ( x e. A , y e. B |-> C ) e. _V )
12	5	rnmpo	|- ran ( x e. A , y e. B |-> C ) = { z | E. x e. A E. y e. B z = C }
13	3	a1i	|- ( ph -> D e. _V )
14		eleq1a	|- ( C e. D -> ( z = C -> z e. D ) )
15	4 14	syl	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C -> z e. D ) )
16	15	rexlimdvva	|- ( ph -> ( E. x e. A E. y e. B z = C -> z e. D ) )
17	16	abssdv	|- ( ph -> { z | E. x e. A E. y e. B z = C } C_ D )
18	13 17	ssexd	|- ( ph -> { z | E. x e. A E. y e. B z = C } e. _V )
19	12 18	eqeltrid	|- ( ph -> ran ( x e. A , y e. B |-> C ) e. _V )
20		funexw	|- ( ( Fun ( x e. A , y e. B |-> C ) /\ dom ( x e. A , y e. B |-> C ) e. _V /\ ran ( x e. A , y e. B |-> C ) e. _V ) -> ( x e. A , y e. B |-> C ) e. _V )
21	6 11 19 20	mp3an2i	|- ( ph -> ( x e. A , y e. B |-> C ) e. _V )