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 
|- ( ph -> A e. D )
fvmptd2f.2 
|- ( ( ph /\ x = A ) -> B e. V )
fvmptd2f.3 
|- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )
fvmptd3f.4 
|- F/_ x F
fvmptd3f.5 
|- F/ x ps
fvmptd3f.6 
|- F/ x ph
Assertion fvmptd3f 
|- ( ph -> ( F = ( x e. D |-> B ) -> ps ) )

Proof

Step Hyp Ref Expression
1 fvmptd2f.1 
 |-  ( ph -> A e. D )
2 fvmptd2f.2 
 |-  ( ( ph /\ x = A ) -> B e. V )
3 fvmptd2f.3 
 |-  ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )
4 fvmptd3f.4 
 |-  F/_ x F
5 fvmptd3f.5 
 |-  F/ x ps
6 fvmptd3f.6 
 |-  F/ x ph
7 nfmpt1 
 |-  F/_ x ( x e. D |-> B )
8 4 7 nfeq 
 |-  F/ x F = ( x e. D |-> B )
9 8 5 nfim 
 |-  F/ x ( F = ( x e. D |-> B ) -> ps )
10 1 elexd 
 |-  ( ph -> A e. _V )
11 isset 
 |-  ( A e. _V <-> E. x x = A )
12 10 11 sylib 
 |-  ( ph -> E. x x = A )
13 fveq1 
 |-  ( F = ( x e. D |-> B ) -> ( F ` A ) = ( ( x e. D |-> B ) ` A ) )
14 simpr 
 |-  ( ( ph /\ x = A ) -> x = A )
15 14 fveq2d 
 |-  ( ( ph /\ x = A ) -> ( ( x e. D |-> B ) ` x ) = ( ( x e. D |-> B ) ` A ) )
16 1 adantr 
 |-  ( ( ph /\ x = A ) -> A e. D )
17 14 16 eqeltrd 
 |-  ( ( ph /\ x = A ) -> x e. D )
18 eqid 
 |-  ( x e. D |-> B ) = ( x e. D |-> B )
19 18 fvmpt2 
 |-  ( ( x e. D /\ B e. V ) -> ( ( x e. D |-> B ) ` x ) = B )
20 17 2 19 syl2anc 
 |-  ( ( ph /\ x = A ) -> ( ( x e. D |-> B ) ` x ) = B )
21 15 20 eqtr3d 
 |-  ( ( ph /\ x = A ) -> ( ( x e. D |-> B ) ` A ) = B )
22 21 eqeq2d 
 |-  ( ( ph /\ x = A ) -> ( ( F ` A ) = ( ( x e. D |-> B ) ` A ) <-> ( F ` A ) = B ) )
23 22 3 sylbid 
 |-  ( ( ph /\ x = A ) -> ( ( F ` A ) = ( ( x e. D |-> B ) ` A ) -> ps ) )
24 13 23 syl5 
 |-  ( ( ph /\ x = A ) -> ( F = ( x e. D |-> B ) -> ps ) )
25 6 9 12 24 exlimdd 
 |-  ( ph -> ( F = ( x e. D |-> B ) -> ps ) )