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	|- F/_ x A
	dmmptssf.2	|- F = ( x e. A |-> B )
Assertion	dmmptssf	|- dom F C_ A

Proof

Step	Hyp	Ref	Expression
1		dmmptssf.1	|- F/_ x A
2		dmmptssf.2	|- F = ( x e. A |-> B )
3	2	dmmpt	|- dom F = { x e. A | B e. _V }
4	1	ssrab2f	|- { x e. A | B e. _V } C_ A
5	3 4	eqsstri	|- dom F C_ A