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	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	fvmptd2f.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑉 )
	fvmptd2f.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝜓 ) )
	fvmptd3f.4	⊢ Ⅎ 𝑥 𝐹
	fvmptd3f.5	⊢ Ⅎ 𝑥 𝜓
	fvmptd3f.6	⊢ Ⅎ 𝑥 𝜑
Assertion	fvmptd3f	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptd2f.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
2		fvmptd2f.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑉 )
3		fvmptd2f.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝜓 ) )
4		fvmptd3f.4	⊢ Ⅎ 𝑥 𝐹
5		fvmptd3f.5	⊢ Ⅎ 𝑥 𝜓
6		fvmptd3f.6	⊢ Ⅎ 𝑥 𝜑
7		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
8	4 7	nfeq	⊢ Ⅎ 𝑥 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
9	8 5	nfim	⊢ Ⅎ 𝑥 ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 )
10	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
11		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
12	10 11	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 = 𝐴 )
13		fveq1	⊢ ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
15	14	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) )
16	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐴 ∈ 𝐷 )
17	14 16	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝐷 )
18		eqid	⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
19	18	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
20	17 2 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
21	15 20	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) = 𝐵 )
22	21	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝐴 ) = 𝐵 ) )
23	22 3	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) ‘ 𝐴 ) → 𝜓 ) )
24	13 23	syl5	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )
25	6 9 12 24	exlimdd	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )

Metamath Proof Explorer

Theorem fvmptd3f

Proof