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

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