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

Metamath Proof Explorer

Theorem fvtresfn

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

		Ref	Expression
	Hypothesis	fvtresfn.f	$⊢ F = (x \in B ⟼ {x ↾}_{V})$
	Assertion	fvtresfn	$⊢ X \in B \to F (X) = {X ↾}_{V}$

Step	Hyp	Ref	Expression
1		fvtresfn.f	$⊢ F = (x \in B ⟼ {x ↾}_{V})$
2		resexg	$⊢ X \in B \to {X ↾}_{V} \in V$
3		reseq1	$⊢ x = X \to {x ↾}_{V} = {X ↾}_{V}$
4	3 1	fvmptg	$⊢ (X \in B \land {X ↾}_{V} \in V) \to F (X) = {X ↾}_{V}$
5	2 4	mpdan	$⊢ X \in B \to F (X) = {X ↾}_{V}$