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	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
	fvmptd.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
	fvmptd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	fvmptd.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	fvmptdf.p	⊢ Ⅎ 𝑥 𝜑
	fvmptdf.a	⊢ Ⅎ 𝑥 𝐴
	fvmptdf.c	⊢ Ⅎ 𝑥 𝐶
Assertion	fvmptdf	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptd.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
2		fvmptd.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
3		fvmptd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
4		fvmptd.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		fvmptdf.p	⊢ Ⅎ 𝑥 𝜑
6		fvmptdf.a	⊢ Ⅎ 𝑥 𝐴
7		fvmptdf.c	⊢ Ⅎ 𝑥 𝐶
8	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) )
9		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
10	9	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11	7	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 )
12		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14	6	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐴
15	5 14	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 = 𝐴 )
16	7	a1i	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → Ⅎ 𝑥 𝐶 )
17		vex	⊢ 𝑦 ∈ V
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝑦 ∈ V )
19		eqtr	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑦 = 𝐴 ) → 𝑥 = 𝐴 )
20	19	ancoms	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝐴 )
21	20 2	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝑦 ) ) → 𝐵 = 𝐶 )
22	21	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑦 = 𝐴 ) ∧ 𝑥 = 𝑦 ) → 𝐵 = 𝐶 )
23	15 16 18 22	csbiedf	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 )
24	5 10 11 3 13 23	csbie2df	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )
25	24 4	eqeltrd	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
26		eqid	⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
27	26	fvmpts	⊢ ( ( 𝐴 ∈ 𝐷 ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
28	3 25 27	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
29	8 28 24	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Metamath Proof Explorer

Theorem fvmptdf

Proof