Metamath Proof Explorer


Theorem dfatopafv2b

Description: Equivalence of function value and ordered pair membership, analogous to fnopfvb or funopfvb . (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion dfatopafv2b ( ( 𝐹 defAt 𝐴𝐵𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dfatbrafv2b ( ( 𝐹 defAt 𝐴𝐵𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵𝐴 𝐹 𝐵 ) )
2 df-br ( 𝐴 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 )
3 1 2 bitrdi ( ( 𝐹 defAt 𝐴𝐵𝑊 ) → ( ( 𝐹 '''' 𝐴 ) = 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐹 ) )