Theorem fvmptss2

Description: A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	fvmptn.1	|- ( x = D -> B = C )
	fvmptn.2	|- F = ( x e. A |-> B )
Assertion	fvmptss2	|- ( F ` D ) C_ C

Proof

Step	Hyp	Ref	Expression
1		fvmptn.1	|- ( x = D -> B = C )
2		fvmptn.2	|- F = ( x e. A |-> B )
3	1	eleq1d	|- ( x = D -> ( B e. _V <-> C e. _V ) )
4	2	dmmpt	|- dom F = { x e. A | B e. _V }
5	3 4	elrab2	|- ( D e. dom F <-> ( D e. A /\ C e. _V ) )
6	1 2	fvmptg	|- ( ( D e. A /\ C e. _V ) -> ( F ` D ) = C )
7		eqimss	|- ( ( F ` D ) = C -> ( F ` D ) C_ C )
8	6 7	syl	|- ( ( D e. A /\ C e. _V ) -> ( F ` D ) C_ C )
9	5 8	sylbi	|- ( D e. dom F -> ( F ` D ) C_ C )
10		ndmfv	|- ( -. D e. dom F -> ( F ` D ) = (/) )
11		0ss	|- (/) C_ C
12	10 11	eqsstrdi	|- ( -. D e. dom F -> ( F ` D ) C_ C )
13	9 12	pm2.61i	|- ( F ` D ) C_ C