Theorem funimassd

Description: Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	funimassd.1	|- F/ x ph
	funimassd.2	|- ( ph -> Fun F )
	funimassd.3	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
Assertion	funimassd	|- ( ph -> ( F " A ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		funimassd.1	|- F/ x ph
2		funimassd.2	|- ( ph -> Fun F )
3		funimassd.3	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
4		fvelima	|- ( ( Fun F /\ y e. ( F " A ) ) -> E. x e. A ( F ` x ) = y )
5	2 4	sylan	|- ( ( ph /\ y e. ( F " A ) ) -> E. x e. A ( F ` x ) = y )
6		nfv	|- F/ x y e. ( F " A )
7	1 6	nfan	|- F/ x ( ph /\ y e. ( F " A ) )
8		nfv	|- F/ x y e. B
9		id	|- ( ( F ` x ) = y -> ( F ` x ) = y )
10	9	eqcomd	|- ( ( F ` x ) = y -> y = ( F ` x ) )
11	10	3ad2ant3	|- ( ( ph /\ x e. A /\ ( F ` x ) = y ) -> y = ( F ` x ) )
12	3	3adant3	|- ( ( ph /\ x e. A /\ ( F ` x ) = y ) -> ( F ` x ) e. B )
13	11 12	eqeltrd	|- ( ( ph /\ x e. A /\ ( F ` x ) = y ) -> y e. B )
14	13	3exp	|- ( ph -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
15	14	adantr	|- ( ( ph /\ y e. ( F " A ) ) -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
16	7 8 15	rexlimd	|- ( ( ph /\ y e. ( F " A ) ) -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
17	5 16	mpd	|- ( ( ph /\ y e. ( F " A ) ) -> y e. B )
18	17	ssd	|- ( ph -> ( F " A ) C_ B )