Theorem dmresv

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

	Ref	Expression
Assertion	dmresv	⊢ dom ( 𝐴 ↾ V ) = dom 𝐴

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( 𝐴 ↾ V ) = ( V ∩ dom 𝐴 )
2		incom	⊢ ( V ∩ dom 𝐴 ) = ( dom 𝐴 ∩ V )
3		inv1	⊢ ( dom 𝐴 ∩ V ) = dom 𝐴
4	1 2 3	3eqtri	⊢ dom ( 𝐴 ↾ V ) = dom 𝐴