Theorem dmmptssf

Description: The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	dmmptssf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dmmptssf.2	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	dmmptssf	$$⊢\mathrm{dom}F\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		dmmptssf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dmmptssf.2	$$⊢F=\left(x\in A⟼B\right)$$
3	2	dmmpt	$$⊢\mathrm{dom}F=\left\{x\in A|B\in \mathrm{V}\right\}$$
4	1	ssrab2f	$$⊢\left\{x\in A|B\in \mathrm{V}\right\}\subseteq A$$
5	3 4	eqsstri	$$⊢\mathrm{dom}F\subseteq A$$