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

Metamath Proof Explorer

Theorem fvmpt

Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011)

Ref Expression
Hypotheses fvmptg.1 ⊢ x = A → B = C
fvmptg.2 ⊢ F = x ∈ D ⟼ B
fvmpt.3 ⊢ C ∈ V
Assertion fvmpt ⊢ A ∈ D → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvmptg.1 ⊢ x = A → B = C
2 fvmptg.2 ⊢ F = x ∈ D ⟼ B
3 fvmpt.3 ⊢ C ∈ V
4 1 2 fvmptg ⊢ A ∈ D ∧ C ∈ V → F ⁡ A = C
5 3 4 mpan2 ⊢ A ∈ D → F ⁡ A = C