Metamath Proof Explorer

Theorem ovmpt4d

Description: Deduction version of ovmpt4g . (This is the operation analogue of fvmpt2d .) (Contributed by Zhi Wang, 9-Oct-2025)

Ref Expression
Hypotheses ovmpt4d.1 ⊢ φ → F = x ∈ A , y ∈ B ⟼ C
ovmpt4d.2 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ V
Assertion ovmpt4d ⊢ φ ∧ x ∈ A ∧ y ∈ B → x F y = C

Proof

Step Hyp Ref Expression
1 ovmpt4d.1 ⊢ φ → F = x ∈ A , y ∈ B ⟼ C
2 ovmpt4d.2 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ V
3 1 oveqdr ⊢ φ ∧ x ∈ A ∧ y ∈ B → x F y = x x ∈ A , y ∈ B ⟼ C y
4 simprl ⊢ φ ∧ x ∈ A ∧ y ∈ B → x ∈ A
5 simprr ⊢ φ ∧ x ∈ A ∧ y ∈ B → y ∈ B
6 eqid ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ A , y ∈ B ⟼ C
7 6 ovmpt4g ⊢ x ∈ A ∧ y ∈ B ∧ C ∈ V → x x ∈ A , y ∈ B ⟼ C y = C
8 4 5 2 7 syl3anc ⊢ φ ∧ x ∈ A ∧ y ∈ B → x x ∈ A , y ∈ B ⟼ C y = C
9 3 8 eqtrd ⊢ φ ∧ x ∈ A ∧ y ∈ B → x F y = C