Theorem fvtresfn

Description: Functionality of a tuple-restriction function. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	fvtresfn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
Assertion	fvtresfn	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ↾ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		fvtresfn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
2		resexg	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ↾ 𝑉 ) ∈ V )
3		reseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ↾ 𝑉 ) = ( 𝑋 ↾ 𝑉 ) )
4	3 1	fvmptg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ↾ 𝑉 ) ∈ V ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ↾ 𝑉 ) )
5	2 4	mpdan	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ↾ 𝑉 ) )