Metamath Proof Explorer


Theorem funbrafv2b

Description: Function value in terms of a binary relation, analogous to funbrfv2b . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion funbrafv2b ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 funrel ( Fun 𝐹 → Rel 𝐹 )
2 releldm ( ( Rel 𝐹𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
3 2 ex ( Rel 𝐹 → ( 𝐴 𝐹 𝐵𝐴 ∈ dom 𝐹 ) )
4 1 3 syl ( Fun 𝐹 → ( 𝐴 𝐹 𝐵𝐴 ∈ dom 𝐹 ) )
5 4 pm4.71rd ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 ↔ ( 𝐴 ∈ dom 𝐹𝐴 𝐹 𝐵 ) ) )
6 funbrafvb ( ( Fun 𝐹𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ''' 𝐴 ) = 𝐵𝐴 𝐹 𝐵 ) )
7 6 pm5.32da ( Fun 𝐹 → ( ( 𝐴 ∈ dom 𝐹 ∧ ( 𝐹 ''' 𝐴 ) = 𝐵 ) ↔ ( 𝐴 ∈ dom 𝐹𝐴 𝐹 𝐵 ) ) )
8 5 7 bitr4d ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ( 𝐹 ''' 𝐴 ) = 𝐵 ) ) )