Theorem fnotaovb

Description: Equivalence of operation value and ordered triple membership, analogous to fnopfvb . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	fnotaovb	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( (( 𝐶 𝐹 𝐷 )) = 𝑅 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) )
2		fnopafvb	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( ( 𝐹 ''' ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑅 ↔ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 ) )
3	1 2	sylan2	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐹 ''' ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑅 ↔ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 ) )
4	3	3impb	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( ( 𝐹 ''' ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑅 ↔ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 ) )
5		df-aov	⊢ (( 𝐶 𝐹 𝐷 )) = ( 𝐹 ''' ⟨ 𝐶 , 𝐷 ⟩ )
6	5	eqeq1i	⊢ ( (( 𝐶 𝐹 𝐷 )) = 𝑅 ↔ ( 𝐹 ''' ⟨ 𝐶 , 𝐷 ⟩ ) = 𝑅 )
7		df-ot	⊢ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩
8	7	eleq1i	⊢ ( ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ↔ ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑅 ⟩ ∈ 𝐹 )
9	4 6 8	3bitr4g	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( (( 𝐶 𝐹 𝐷 )) = 𝑅 ↔ ⟨ 𝐶 , 𝐷 , 𝑅 ⟩ ∈ 𝐹 ) )