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 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
fvmptg.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
fvmpt.3 ⊢ 𝐶 ∈ V
Assertion fvmpt ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 fvmptg.1 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2 fvmptg.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3 fvmpt.3 ⊢ 𝐶 ∈ V
4 1 2 fvmptg ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
5 3 4 mpan2 ⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )