This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnopfv

Description: Ordered pair with function value. Part of Theorem 4.3(i) of Monk1 p. 41. (Contributed by NM, 30-Sep-2004)

Ref Expression
Assertion fnopfv ⊢ F Fn A ∧ B ∈ A → B F ⁡ B ∈ F

Proof

Step Hyp Ref Expression
1 funfvop ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → B F ⁡ B ∈ F
2 1 funfni ⊢ F Fn A ∧ B ∈ A → B F ⁡ B ∈ F