Theorem fvtresfn

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

	Ref	Expression
Hypothesis	fvtresfn.f	$$⊢F=\left(x\in B⟼{x\upharpoonright }_V\right)$$
Assertion	fvtresfn	$$⊢X\in B\to F\left(X\right)={X\upharpoonright }_V$$

Proof

Step	Hyp	Ref	Expression
1		fvtresfn.f	$$⊢F=\left(x\in B⟼{x\upharpoonright }_V\right)$$
2		resexg	$$⊢X\in B\to {X\upharpoonright }_V\in \mathrm{V}$$
3		reseq1	$$⊢x=X\to {x\upharpoonright }_V={X\upharpoonright }_V$$
4	3 1	fvmptg	$$⊢\left(X\in B\wedge {X\upharpoonright }_V\in \mathrm{V}\right)\to F\left(X\right)={X\upharpoonright }_V$$
5	2 4	mpdan	$$⊢X\in B\to F\left(X\right)={X\upharpoonright }_V$$