Metamath Proof Explorer

Theorem funbrafv22b

Description: Equivalence of function value and binary relation, analogous to funbrfvb . (Contributed by AV, 6-Sep-2022)

Ref Expression
Assertion funbrafv22b ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F '''' A = B ↔ A F B

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 fnbrafv2b ⊢ F Fn dom ⁡ F ∧ A ∈ dom ⁡ F → F '''' A = B ↔ A F B
3 1 2 sylanb ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F '''' A = B ↔ A F B