Metamath Proof Explorer


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 ) )