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	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( ( 𝐶 𝐹 𝐷 ) = 𝑅 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fnbrovb	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 𝐹 𝐷 ) = 𝑅 ↔ ⟨ 𝐶 , 𝐷 ⟩ 𝐹 𝑅 ) )
2		df-br	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ 𝐹 𝑅 ↔ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 )
3	2	a1i	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ 𝐹 𝑅 ↔ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 ) )
4		df-ot	⊢ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩
5	4	eqcomi	⊢ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ = ⟨ 𝐶 , 𝐷 , 𝑅 ⟩
6	5	eleq1i	⊢ ( ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 )
7	6	a1i	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ) )
8	1 3 7	3bitrd	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 𝐹 𝐷 ) = 𝑅 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ) )
9	8	3impb	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( ( 𝐶 𝐹 𝐷 ) = 𝑅 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ) )