Metamath Proof Explorer


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 ( 𝐴𝐵 ) ⊆ dom 𝐴

Proof

Step Hyp Ref Expression
1 resss ( 𝐴𝐵 ) ⊆ 𝐴
2 dmss ( ( 𝐴𝐵 ) ⊆ 𝐴 → dom ( 𝐴𝐵 ) ⊆ dom 𝐴 )
3 1 2 ax-mp dom ( 𝐴𝐵 ) ⊆ dom 𝐴