Theorem mpoexwd

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

	Ref	Expression
Hypotheses	mpoexwd.1	⊢ 𝐴 ∈ V
	mpoexwd.2	⊢ 𝐵 ∈ V
	mpoexwd.3	⊢ 𝐷 ∈ V
	mpoexwd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
Assertion	mpoexwd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		mpoexwd.1	⊢ 𝐴 ∈ V
2		mpoexwd.2	⊢ 𝐵 ∈ V
3		mpoexwd.3	⊢ 𝐷 ∈ V
4		mpoexwd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
6	5	mpofun	⊢ Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
7	4	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 )
8	5	dmmpoga	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝐴 × 𝐵 ) )
9	7 8	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝐴 × 𝐵 ) )
10	1 2	xpex	⊢ ( 𝐴 × 𝐵 ) ∈ V
11	9 10	eqeltrdi	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
12	5	rnmpo	⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 }
13	3	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
14		eleq1a	⊢ ( 𝐶 ∈ 𝐷 → ( 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
15	4 14	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
16	15	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 → 𝑧 ∈ 𝐷 ) )
17	16	abssdv	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ⊆ 𝐷 )
18	13 17	ssexd	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ∈ V )
19	12 18	eqeltrid	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
20		funexw	⊢ ( ( Fun ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∧ dom ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ∧ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
21	6 11 19 20	mp3an2i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )