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

Metamath Proof Explorer

Theorem fvmptd3f

Proof