Theorem dmss

Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994)

	Ref	Expression
Assertion	dmss	$$⊢A\subseteq B\to \mathrm{dom}A\subseteq \mathrm{dom}B$$

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢A\subseteq B\to \left(⟨x,y⟩\in A\to ⟨x,y⟩\in B\right)$$
2	1	eximdv	$$⊢A\subseteq B\to \left(\exists y⟨x,y⟩\in A\to \exists y⟨x,y⟩\in B\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	eldm2	$$⊢x\in \mathrm{dom}A\leftrightarrow \exists y⟨x,y⟩\in A$$
5	3	eldm2	$$⊢x\in \mathrm{dom}B\leftrightarrow \exists y⟨x,y⟩\in B$$
6	2 4 5	3imtr4g	$$⊢A\subseteq B\to \left(x\in \mathrm{dom}A\to x\in \mathrm{dom}B\right)$$
7	6	ssrdv	$$⊢A\subseteq B\to \mathrm{dom}A\subseteq \mathrm{dom}B$$