Metamath Proof Explorer

Theorem fvmptd3f

Description: Alternate deduction version of fvmpt with three non-freeness hypotheses instead of distinct variable conditions. (Contributed 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 → ψ
fvmptd3f.4 ⊢ Ⅎ _ x F
fvmptd3f.5 ⊢ Ⅎ x ψ
fvmptd3f.6 ⊢ Ⅎ x φ
Assertion fvmptd3f ⊢ φ → 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 fvmptd3f.4 ⊢ Ⅎ _ x F
5 fvmptd3f.5 ⊢ Ⅎ x ψ
6 fvmptd3f.6 ⊢ Ⅎ x φ
7 nfmpt1 ⊢ Ⅎ _ x x ∈ D ⟼ B
8 4 7 nfeq ⊢ Ⅎ x F = x ∈ D ⟼ B
9 8 5 nfim ⊢ Ⅎ x F = x ∈ D ⟼ B → ψ
10 1 elexd ⊢ φ → A ∈ V
11 isset ⊢ A ∈ V ↔ ∃ x x = A
12 10 11 sylib ⊢ φ → ∃ x x = A
13 fveq1 ⊢ F = x ∈ D ⟼ B → F ⁡ A = x ∈ D ⟼ B ⁡ A
14 simpr ⊢ φ ∧ x = A → x = A
15 14 fveq2d ⊢ φ ∧ x = A → x ∈ D ⟼ B ⁡ x = x ∈ D ⟼ B ⁡ A
16 1 adantr ⊢ φ ∧ x = A → A ∈ D
17 14 16 eqeltrd ⊢ φ ∧ x = A → x ∈ D
18 eqid ⊢ x ∈ D ⟼ B = x ∈ D ⟼ B
19 18 fvmpt2 ⊢ x ∈ D ∧ B ∈ V → x ∈ D ⟼ B ⁡ x = B
20 17 2 19 syl2anc ⊢ φ ∧ x = A → x ∈ D ⟼ B ⁡ x = B
21 15 20 eqtr3d ⊢ φ ∧ x = A → x ∈ D ⟼ B ⁡ A = B
22 21 eqeq2d ⊢ φ ∧ x = A → F ⁡ A = x ∈ D ⟼ B ⁡ A ↔ F ⁡ A = B
23 22 3 sylbid ⊢ φ ∧ x = A → F ⁡ A = x ∈ D ⟼ B ⁡ A → ψ
24 13 23 syl5 ⊢ φ ∧ x = A → F = x ∈ D ⟼ B → ψ
25 6 9 12 24 exlimdd ⊢ φ → F = x ∈ D ⟼ B → ψ