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

Metamath Proof Explorer

Theorem funfvop

Description: Ordered pair with function value. Part of Theorem 4.3(i) of Monk1 p. 41. (Contributed by NM, 14-Oct-1996)

Ref Expression
Assertion funfvop ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F ⁡ A ∈ F

Proof

Step Hyp Ref Expression
1 eqid ⊢ F ⁡ A = F ⁡ A
2 funopfvb ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A = F ⁡ A ↔ A F ⁡ A ∈ F
3 1 2 mpbii ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F ⁡ A ∈ F