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

Metamath Proof Explorer

Theorem fvmptd4

Description: Deduction version of fvmpt (where the substitution hypothesis does not have the antecedent ph ). (Contributed by SN, 26-Jul-2024)

Ref Expression
Hypotheses fvmptd4.1 ⊢ x = A → B = C
fvmptd4.2 ⊢ φ → F = x ∈ D ⟼ B
fvmptd4.3 ⊢ φ → A ∈ D
fvmptd4.4 ⊢ φ → C ∈ V
Assertion fvmptd4 ⊢ φ → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvmptd4.1 ⊢ x = A → B = C
2 fvmptd4.2 ⊢ φ → F = x ∈ D ⟼ B
3 fvmptd4.3 ⊢ φ → A ∈ D
4 fvmptd4.4 ⊢ φ → C ∈ V
5 1 adantl ⊢ φ ∧ x = A → B = C
6 2 5 3 4 fvmptd ⊢ φ → F ⁡ A = C