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	|- ( 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 ) )