ovmpt4d

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

Step	Hyp	Ref	Expression
1		ovmpt4d.1	$⊢ φ \to F = (x \in A, y \in B ⟼ C)$
2		ovmpt4d.2	$⊢ (φ \land (x \in A \land y \in B)) \to C \in V$
3	1	oveqdr	$⊢ (φ \land (x \in A \land y \in B)) \to x F y = x (x \in A, y \in B ⟼ C) y$
4		simprl	$⊢ (φ \land (x \in A \land y \in B)) \to x \in A$
5		simprr	$⊢ (φ \land (x \in A \land y \in B)) \to y \in B$
6		eqid	$⊢ (x \in A, y \in B ⟼ C) = (x \in A, y \in B ⟼ C)$
7	6	ovmpt4g	$⊢ (x \in A \land y \in B \land C \in V) \to x (x \in A, y \in B ⟼ C) y = C$
8	4 5 2 7	syl3anc	$⊢ (φ \land (x \in A \land y \in B)) \to x (x \in A, y \in B ⟼ C) y = C$
9	3 8	eqtrd	$⊢ (φ \land (x \in A \land y \in B)) \to x F y = C$

Metamath Proof Explorer