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 e. A |-> B )
Assertion	dmmptss	|- dom F C_ A

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	|- F = ( x e. A |-> B )
2	1	dmmpt	|- dom F = { x e. A | B e. _V }
3	2	ssrab3	|- dom F C_ A