ovelimab

Description: Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013) (Revised by Mario Carneiro, 29-Jan-2014)

		Ref	Expression
	Assertion	ovelimab	$⊢ (F Fn A \land B \times C \subseteq A) \to (D \in F [B \times C] \leftrightarrow \exists x \in B \exists y \in C D = x F y)$

Step	Hyp	Ref	Expression
1		fvelimab	$⊢ (F Fn A \land B \times C \subseteq A) \to (D \in F [B \times C] \leftrightarrow \exists z \in (B \times C) F (z) = D)$
2		fveq2	$⊢ z = ⟨x, y⟩ \to F (z) = F (⟨x, y⟩)$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	2 3	eqtr4di	$⊢ z = ⟨x, y⟩ \to F (z) = x F y$
5	4	eqeq1d	$⊢ z = ⟨x, y⟩ \to (F (z) = D \leftrightarrow x F y = D)$
6		eqcom	$⊢ x F y = D \leftrightarrow D = x F y$
7	5 6	bitrdi	$⊢ z = ⟨x, y⟩ \to (F (z) = D \leftrightarrow D = x F y)$
8	7	rexxp	$⊢ \exists z \in (B \times C) F (z) = D \leftrightarrow \exists x \in B \exists y \in C D = x F y$
9	1 8	bitrdi	$⊢ (F Fn A \land B \times C \subseteq A) \to (D \in F [B \times C] \leftrightarrow \exists x \in B \exists y \in C D = x F y)$

Metamath Proof Explorer