This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvmpt3

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	fvmpt3.a	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
	fvmpt3.b	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
	fvmpt3.c	⊢ ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 )
Assertion	fvmpt3	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmpt3.a	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2		fvmpt3.b	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3		fvmpt3.c	⊢ ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 )
4	1	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ 𝑉 ↔ 𝐶 ∈ 𝑉 ) )
5	4 3	vtoclga	⊢ ( 𝐴 ∈ 𝐷 → 𝐶 ∈ 𝑉 )
6	1 2	fvmptg	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
7	5 6	mpdan	⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )