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

Metamath Proof Explorer

Theorem fvmptg

Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 fvmptg.1 ⊢ x = A → B = C
2 fvmptg.2 ⊢ F = x ∈ D ⟼ B
3 eqid ⊢ C = C
4 1 eqeq2d ⊢ x = A → y = B ↔ y = C
5 eqeq1 ⊢ y = C → y = C ↔ C = C
6 moeq ⊢ ∃* y y = B
7 6 a1i ⊢ x ∈ D → ∃* y y = B
8 df-mpt ⊢ x ∈ D ⟼ B = x y | x ∈ D ∧ y = B
9 2 8 eqtri ⊢ F = x y | x ∈ D ∧ y = B
10 4 5 7 9 fvopab3ig ⊢ A ∈ D ∧ C ∈ R → C = C → F ⁡ A = C
11 3 10 mpi ⊢ A ∈ D ∧ C ∈ R → F ⁡ A = C