Metamath Proof Explorer


Theorem fvmptd3f

Description: Alternate deduction version of fvmpt with three nonfreeness 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 ψ