Theorem dmresss

Description: The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	dmresss	⊢ dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 )
2		inss2	⊢ ( 𝐵 ∩ dom 𝐴 ) ⊆ dom 𝐴
3	1 2	eqsstri	⊢ dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴