# Metamath Proof Explorer

## Theorem fvmpt2d

Description: Deduction version of fvmpt2 . (Contributed by Thierry Arnoux, 8-Dec-2016)

Ref Expression
Hypotheses fvmpt2d.1 ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{B}\right)$
fvmpt2d.4 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
Assertion fvmpt2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={B}$

### Proof

Step Hyp Ref Expression
1 fvmpt2d.1 ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{B}\right)$
2 fvmpt2d.4 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
3 1 fveq1d ${⊢}{\phi }\to {F}\left({x}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
4 3 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
5 id ${⊢}{x}\in {A}\to {x}\in {A}$
6 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
7 6 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in {V}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
8 5 2 7 syl2an2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
9 4 8 eqtrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={B}$