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

Metamath Proof Explorer

Theorem fvmpt2d

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

Ref Expression
Hypotheses fvmpt2d.1 ⊢ φ → F = x ∈ A ⟼ B
fvmpt2d.4 ⊢ φ ∧ x ∈ A → B ∈ V
Assertion fvmpt2d ⊢ φ ∧ x ∈ A → F ⁡ x = B

Proof

Step Hyp Ref Expression
1 fvmpt2d.1 ⊢ φ → F = x ∈ A ⟼ B
2 fvmpt2d.4 ⊢ φ ∧ x ∈ A → B ∈ V
3 1 fveq1d ⊢ φ → F ⁡ x = x ∈ A ⟼ B ⁡ x
4 3 adantr ⊢ φ ∧ x ∈ A → F ⁡ x = x ∈ A ⟼ B ⁡ x
5 id ⊢ x ∈ A → x ∈ A
6 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
7 6 fvmpt2 ⊢ x ∈ A ∧ B ∈ V → x ∈ A ⟼ B ⁡ x = B
8 5 2 7 syl2an2 ⊢ φ ∧ x ∈ A → x ∈ A ⟼ B ⁡ x = B
9 4 8 eqtrd ⊢ φ ∧ x ∈ A → F ⁡ x = B