Theorem fvmptdf

Description: Deduction version of fvmptd using bound-variable hypotheses instead of distinct variable conditions. (Contributed by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	fvmptd.1	$$⊢\phi \to F=\left(x\in D⟼B\right)$$
	fvmptd.2	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
	fvmptd.3	$$⊢\phi \to A\in D$$
	fvmptd.4	$$⊢\phi \to C\in V$$
	fvmptdf.p	$$⊢Ⅎx\phi$$
	fvmptdf.a	$$⊢\underset{\_}{Ⅎ}xA$$
	fvmptdf.c	$$⊢\underset{\_}{Ⅎ}xC$$
Assertion	fvmptdf	$$⊢\phi \to F\left(A\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		fvmptd.1	$$⊢\phi \to F=\left(x\in D⟼B\right)$$
2		fvmptd.2	$$⊢\left(\phi \wedge x=A\right)\to B=C$$
3		fvmptd.3	$$⊢\phi \to A\in D$$
4		fvmptd.4	$$⊢\phi \to C\in V$$
5		fvmptdf.p	$$⊢Ⅎx\phi$$
6		fvmptdf.a	$$⊢\underset{\_}{Ⅎ}xA$$
7		fvmptdf.c	$$⊢\underset{\_}{Ⅎ}xC$$
8	1	fveq1d	$$⊢\phi \to F\left(A\right)=\left(x\in D⟼B\right)\left(A\right)$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
10	9	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}x⦋y/x⦌B$$
11	7	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$
12		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
13	12	adantl	$$⊢\left(\phi \wedge x=y\right)\to B=⦋y/x⦌B$$
14	6	nfeq2	$$⊢Ⅎxy=A$$
15	5 14	nfan	$$⊢Ⅎx\left(\phi \wedge y=A\right)$$
16	7	a1i	$$⊢\left(\phi \wedge y=A\right)\to \underset{\_}{Ⅎ}xC$$
17		vex	$$⊢y\in \mathrm{V}$$
18	17	a1i	$$⊢\left(\phi \wedge y=A\right)\to y\in \mathrm{V}$$
19		eqtr	$$⊢\left(x=y\wedge y=A\right)\to x=A$$
20	19	ancoms	$$⊢\left(y=A\wedge x=y\right)\to x=A$$
21	20 2	sylan2	$$⊢\left(\phi \wedge \left(y=A\wedge x=y\right)\right)\to B=C$$
22	21	anassrs	$$⊢\left(\left(\phi \wedge y=A\right)\wedge x=y\right)\to B=C$$
23	15 16 18 22	csbiedf	$$⊢\left(\phi \wedge y=A\right)\to ⦋y/x⦌B=C$$
24	5 10 11 3 13 23	csbie2df	$$⊢\phi \to ⦋A/x⦌B=C$$
25	24 4	eqeltrd	$$⊢\phi \to ⦋A/x⦌B\in V$$
26		eqid	$$⊢\left(x\in D⟼B\right)=\left(x\in D⟼B\right)$$
27	26	fvmpts	$$⊢\left(A\in D\wedge ⦋A/x⦌B\in V\right)\to \left(x\in D⟼B\right)\left(A\right)=⦋A/x⦌B$$
28	3 25 27	syl2anc	$$⊢\phi \to \left(x\in D⟼B\right)\left(A\right)=⦋A/x⦌B$$
29	8 28 24	3eqtrd	$$⊢\phi \to F\left(A\right)=C$$