Metamath Proof Explorer

Theorem mpoexwd

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

Ref Expression
Hypotheses mpoexwd.1 ⊢ A ∈ V
mpoexwd.2 ⊢ B ∈ V
mpoexwd.3 ⊢ D ∈ V
mpoexwd.4 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ D
Assertion mpoexwd ⊢ φ → x ∈ A , y ∈ B ⟼ C ∈ V

Proof

Step Hyp Ref Expression
1 mpoexwd.1 ⊢ A ∈ V
2 mpoexwd.2 ⊢ B ∈ V
3 mpoexwd.3 ⊢ D ∈ V
4 mpoexwd.4 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ D
5 eqid ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ C
6 5 mpofun ⊢ Fun ⁡ x ∈ A , y ∈ B ⟼ C
7 4 ralrimivva ⊢ φ → ∀ x ∈ A ∀ y ∈ B C ∈ D
8 5 dmmpoga ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D → dom ⁡ x ∈ A , y ∈ B ⟼ C = A × B
9 7 8 syl ⊢ φ → dom ⁡ x ∈ A , y ∈ B ⟼ C = A × B
10 1 2 xpex ⊢ A × B ∈ V
11 9 10 eqeltrdi ⊢ φ → dom ⁡ x ∈ A , y ∈ B ⟼ C ∈ V
12 5 rnmpo ⊢ ran ⁡ x ∈ A , y ∈ B ⟼ C = z | ∃ x ∈ A ∃ y ∈ B z = C
13 3 a1i ⊢ φ → D ∈ V
14 eleq1a ⊢ C ∈ D → z = C → z ∈ D
15 4 14 syl ⊢ φ ∧ x ∈ A ∧ y ∈ B → z = C → z ∈ D
16 15 rexlimdvva ⊢ φ → ∃ x ∈ A ∃ y ∈ B z = C → z ∈ D
17 16 abssdv ⊢ φ → z | ∃ x ∈ A ∃ y ∈ B z = C ⊆ D
18 13 17 ssexd ⊢ φ → z | ∃ x ∈ A ∃ y ∈ B z = C ∈ V
19 12 18 eqeltrid ⊢ φ → ran ⁡ x ∈ A , y ∈ B ⟼ C ∈ V
20 funexw ⊢ Fun ⁡ x ∈ A , y ∈ B ⟼ C ∧ dom ⁡ x ∈ A , y ∈ B ⟼ C ∈ V ∧ ran ⁡ x ∈ A , y ∈ B ⟼ C ∈ V → x ∈ A , y ∈ B ⟼ C ∈ V
21 6 11 19 20 mp3an2i ⊢ φ → x ∈ A , y ∈ B ⟼ C ∈ V