Theorem funimaeq

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	funimaeq.x	|- F/ x ph
	funimaeq.f	|- ( ph -> Fun F )
	funimaeq.g	|- ( ph -> Fun G )
	funimaeq.a	|- ( ph -> A C_ dom F )
	funimaeq.d	|- ( ph -> A C_ dom G )
	funimaeq.e	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
Assertion	funimaeq	|- ( ph -> ( F " A ) = ( G " A ) )

Proof

Step	Hyp	Ref	Expression
1		funimaeq.x	|- F/ x ph
2		funimaeq.f	|- ( ph -> Fun F )
3		funimaeq.g	|- ( ph -> Fun G )
4		funimaeq.a	|- ( ph -> A C_ dom F )
5		funimaeq.d	|- ( ph -> A C_ dom G )
6		funimaeq.e	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
7	3	funfnd	|- ( ph -> G Fn dom G )
8	7	adantr	|- ( ( ph /\ x e. A ) -> G Fn dom G )
9	5	adantr	|- ( ( ph /\ x e. A ) -> A C_ dom G )
10		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
11		fnfvima	|- ( ( G Fn dom G /\ A C_ dom G /\ x e. A ) -> ( G ` x ) e. ( G " A ) )
12	8 9 10 11	syl3anc	|- ( ( ph /\ x e. A ) -> ( G ` x ) e. ( G " A ) )
13	6 12	eqeltrd	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. ( G " A ) )
14	1 2 13	funimassd	|- ( ph -> ( F " A ) C_ ( G " A ) )
15	2	funfnd	|- ( ph -> F Fn dom F )
16	15	adantr	|- ( ( ph /\ x e. A ) -> F Fn dom F )
17	4	adantr	|- ( ( ph /\ x e. A ) -> A C_ dom F )
18		fnfvima	|- ( ( F Fn dom F /\ A C_ dom F /\ x e. A ) -> ( F ` x ) e. ( F " A ) )
19	16 17 10 18	syl3anc	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. ( F " A ) )
20	6 19	eqeltrrd	|- ( ( ph /\ x e. A ) -> ( G ` x ) e. ( F " A ) )
21	1 3 20	funimassd	|- ( ph -> ( G " A ) C_ ( F " A ) )
22	14 21	eqssd	|- ( ph -> ( F " A ) = ( G " A ) )