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

Metamath Proof Explorer

Theorem fvmptmap

Description: Special case of fvmpt for operator theorems. (Contributed by NM, 27-Nov-2007)

Ref Expression
Hypotheses fvmptmap.1 ⊢ C ∈ V
fvmptmap.2 ⊢ D ∈ V
fvmptmap.3 ⊢ R ∈ V
fvmptmap.4 ⊢ x = A → B = C
fvmptmap.5 ⊢ F = x ∈ R D ⟼ B
Assertion fvmptmap ⊢ A : D ⟶ R → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvmptmap.1 ⊢ C ∈ V
2 fvmptmap.2 ⊢ D ∈ V
3 fvmptmap.3 ⊢ R ∈ V
4 fvmptmap.4 ⊢ x = A → B = C
5 fvmptmap.5 ⊢ F = x ∈ R D ⟼ B
6 3 2 elmap ⊢ A ∈ R D ↔ A : D ⟶ R
7 4 5 1 fvmpt ⊢ A ∈ R D → F ⁡ A = C
8 6 7 sylbir ⊢ A : D ⟶ R → F ⁡ A = C