Theorem fnopafvb

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

	Ref	Expression
Assertion	fnopafvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fnbrafvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶 ↔ 𝐵 𝐹 𝐶 ) )
2		df-br	⊢ ( 𝐵 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 )
3	1 2	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) )