dmss

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

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

Metamath Proof Explorer