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

Metamath Proof Explorer

Theorem fvmptd2f

Description: Alternate deduction version of fvmpt , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017) (Proof shortened by AV, 19-Jan-2022)

Ref Expression
Hypotheses fvmptd2f.1 ⊢ φ → A ∈ D
fvmptd2f.2 ⊢ φ ∧ x = A → B ∈ V
fvmptd2f.3 ⊢ φ ∧ x = A → F ⁡ A = B → ψ
fvmptd2f.4 ⊢ Ⅎ _ x F
fvmptd2f.5 ⊢ Ⅎ x ψ
Assertion fvmptd2f ⊢ φ → F = x ∈ D ⟼ B → ψ

Proof

Step Hyp Ref Expression
1 fvmptd2f.1 ⊢ φ → A ∈ D
2 fvmptd2f.2 ⊢ φ ∧ x = A → B ∈ V
3 fvmptd2f.3 ⊢ φ ∧ x = A → F ⁡ A = B → ψ
4 fvmptd2f.4 ⊢ Ⅎ _ x F
5 fvmptd2f.5 ⊢ Ⅎ x ψ
6 nfv ⊢ Ⅎ x φ
7 1 2 3 4 5 6 fvmptd3f ⊢ φ → F = x ∈ D ⟼ B → ψ