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

Metamath Proof Explorer

Theorem fvmptdf

Description: Deduction version of fvmptd using bound-variable hypotheses instead of distinct variable conditions. (Contributed by AV, 29-Mar-2024)

Ref Expression
Hypotheses fvmptd.1 ⊢ φ → F = x ∈ D ⟼ B
fvmptd.2 ⊢ φ ∧ x = A → B = C
fvmptd.3 ⊢ φ → A ∈ D
fvmptd.4 ⊢ φ → C ∈ V
fvmptdf.p ⊢ Ⅎ x φ
fvmptdf.a ⊢ Ⅎ _ x A
fvmptdf.c ⊢ Ⅎ _ x C
Assertion fvmptdf ⊢ φ → F ⁡ A = C

Proof

Step Hyp Ref Expression
1 fvmptd.1 ⊢ φ → F = x ∈ D ⟼ B
2 fvmptd.2 ⊢ φ ∧ x = A → B = C
3 fvmptd.3 ⊢ φ → A ∈ D
4 fvmptd.4 ⊢ φ → C ∈ V
5 fvmptdf.p ⊢ Ⅎ x φ
6 fvmptdf.a ⊢ Ⅎ _ x A
7 fvmptdf.c ⊢ Ⅎ _ x C
8 1 fveq1d ⊢ φ → F ⁡ A = x ∈ D ⟼ B ⁡ A
9 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
10 9 a1i ⊢ φ → Ⅎ _ x ⦋ y / x⦌ B
11 7 a1i ⊢ φ → Ⅎ _ x C
12 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
13 12 adantl ⊢ φ ∧ x = y → B = ⦋ y / x⦌ B
14 6 nfeq2 ⊢ Ⅎ x y = A
15 5 14 nfan ⊢ Ⅎ x φ ∧ y = A
16 7 a1i ⊢ φ ∧ y = A → Ⅎ _ x C
17 vex ⊢ y ∈ V
18 17 a1i ⊢ φ ∧ y = A → y ∈ V
19 eqtr ⊢ x = y ∧ y = A → x = A
20 19 ancoms ⊢ y = A ∧ x = y → x = A
21 20 2 sylan2 ⊢ φ ∧ y = A ∧ x = y → B = C
22 21 anassrs ⊢ φ ∧ y = A ∧ x = y → B = C
23 15 16 18 22 csbiedf ⊢ φ ∧ y = A → ⦋ y / x⦌ B = C
24 5 10 11 3 13 23 csbie2df ⊢ φ → ⦋ A / x⦌ B = C
25 24 4 eqeltrd ⊢ φ → ⦋ A / x⦌ B ∈ V
26 eqid ⊢ x ∈ D ⟼ B = x ∈ D ⟼ B
27 26 fvmpts ⊢ A ∈ D ∧ ⦋ A / x⦌ B ∈ V → x ∈ D ⟼ B ⁡ A = ⦋ A / x⦌ B
28 3 25 27 syl2anc ⊢ φ → x ∈ D ⟼ B ⁡ A = ⦋ A / x⦌ B
29 8 28 24 3eqtrd ⊢ φ → F ⁡ A = C