This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovmpot

Description: The value of an operation is equal to the value of the same operation expressed in maps-to notation. (Contributed by GG, 16-Mar-2025) (Revised by GG, 13-Apr-2025)

		Ref	Expression
	Assertion	ovmpot	$⊢ (A \in C \land B \in D) \to A (x \in C, y \in D ⟼ x F y) B = A F B$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$⊢ (x = A \land y = B) \to x F y = A F B$
2		eqid	$⊢ (x \in C, y \in D ⟼ x F y) = (x \in C, y \in D ⟼ x F y)$
3		ovex	$⊢ A F B \in V$
4	1 2 3	ovmpoa	$⊢ (A \in C \land B \in D) \to A (x \in C, y \in D ⟼ x F y) B = A F B$