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

Metamath Proof Explorer

Theorem dmresv

Description: The domain of a universal restriction. (Contributed by NM, 14-May-2008)

		Ref	Expression
	Assertion	dmresv	$⊢ dom ({A ↾}_{V}) = dom A$

Step	Hyp	Ref	Expression
1		dmres	$⊢ dom ({A ↾}_{V}) = V \cap dom A$
2		incom	$⊢ V \cap dom A = dom A \cap V$
3		inv1	$⊢ dom A \cap V = dom A$
4	1 2 3	3eqtri	$⊢ dom ({A ↾}_{V}) = dom A$