This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (x \in A ⟼ B)$
	Assertion	dmmptss	$⊢ dom F \subseteq A$

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