Theorem dmmptss

Description: The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013)

	Ref	Expression
Hypothesis	dmmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	dmmptss	$$⊢\mathrm{dom}F\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2	1	dmmpt	$$⊢\mathrm{dom}F=\left\{x\in A|B\in \mathrm{V}\right\}$$
3	2	ssrab3	$$⊢\mathrm{dom}F\subseteq A$$