Theorem dmresss

Description: The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021) Proof shortened and axiom usage reduced. (Proof shortened by AV, 15-May-2025)

	Ref	Expression
Assertion	dmresss	|- dom ( A |` B ) C_ dom A

Proof

Step	Hyp	Ref	Expression
1		resss	|- ( A |` B ) C_ A
2		dmss	|- ( ( A |` B ) C_ A -> dom ( A |` B ) C_ dom A )
3	1 2	ax-mp	|- dom ( A |` B ) C_ dom A