**Description:** Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995)

Ref | Expression | ||
---|---|---|---|

Assertion | fnopfvb | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | fnbrfvb | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 ↔ 𝐵 𝐹 𝐶 ) ) | |

2 | df-br | ⊢ ( 𝐵 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) | |

3 | 1 2 | syl6bb | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝐹 ) ) |