Metamath Proof Explorer

Theorem fnotovb

Description: Equivalence of operation value and ordered triple membership, analogous to fnopfvb . (Contributed by NM, 17-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015) (Proof shortened by BJ, 15-Feb-2022)

		Ref	Expression
	Assertion	fnotovb	$⊢ (F Fn (A \times B) \land C \in A \land D \in B) \to (C F D = R \leftrightarrow ⟨C, D, R⟩ \in F)$

Proof

Step	Hyp	Ref	Expression
1		fnbrovb	$⊢ (F Fn (A \times B) \land (C \in A \land D \in B)) \to (C F D = R \leftrightarrow ⟨C, D⟩ F R)$
2		df-br	$⊢ ⟨C, D⟩ F R \leftrightarrow ⟨⟨C, D⟩, R⟩ \in F$
3	2	a1i	$⊢ (F Fn (A \times B) \land (C \in A \land D \in B)) \to (⟨C, D⟩ F R \leftrightarrow ⟨⟨C, D⟩, R⟩ \in F)$
4		df-ot	$⊢ ⟨C, D, R⟩ = ⟨⟨C, D⟩, R⟩$
5	4	eqcomi	$⊢ ⟨⟨C, D⟩, R⟩ = ⟨C, D, R⟩$
6	5	eleq1i	$⊢ ⟨⟨C, D⟩, R⟩ \in F \leftrightarrow ⟨C, D, R⟩ \in F$
7	6	a1i	$⊢ (F Fn (A \times B) \land (C \in A \land D \in B)) \to (⟨⟨C, D⟩, R⟩ \in F \leftrightarrow ⟨C, D, R⟩ \in F)$
8	1 3 7	3bitrd	$⊢ (F Fn (A \times B) \land (C \in A \land D \in B)) \to (C F D = R \leftrightarrow ⟨C, D, R⟩ \in F)$
9	8	3impb	$⊢ (F Fn (A \times B) \land C \in A \land D \in B) \to (C F D = R \leftrightarrow ⟨C, D, R⟩ \in F)$