This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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