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

Metamath Proof Explorer

Theorem elimampt

Description: Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Hypotheses elimampt.f 
|- F = ( x e. A |-> B )
elimampt.c 
|- ( ph -> C e. W )
elimampt.d 
|- ( ph -> D C_ A )
Assertion elimampt 
|- ( ph -> ( C e. ( F " D ) <-> E. x e. D C = B ) )

Proof

Step Hyp Ref Expression
1 elimampt.f 
 |-  F = ( x e. A |-> B )
2 elimampt.c 
 |-  ( ph -> C e. W )
3 elimampt.d 
 |-  ( ph -> D C_ A )
4 df-ima 
 |-  ( F " D ) = ran ( F |` D )
5 4 eleq2i 
 |-  ( C e. ( F " D ) <-> C e. ran ( F |` D ) )
6 1 reseq1i 
 |-  ( F |` D ) = ( ( x e. A |-> B ) |` D )
7 resmpt 
 |-  ( D C_ A -> ( ( x e. A |-> B ) |` D ) = ( x e. D |-> B ) )
8 6 7 eqtrid 
 |-  ( D C_ A -> ( F |` D ) = ( x e. D |-> B ) )
9 8 rneqd 
 |-  ( D C_ A -> ran ( F |` D ) = ran ( x e. D |-> B ) )
10 9 eleq2d 
 |-  ( D C_ A -> ( C e. ran ( F |` D ) <-> C e. ran ( x e. D |-> B ) ) )
11 3 10 syl 
 |-  ( ph -> ( C e. ran ( F |` D ) <-> C e. ran ( x e. D |-> B ) ) )
12 eqid 
 |-  ( x e. D |-> B ) = ( x e. D |-> B )
13 12 elrnmpt 
 |-  ( C e. W -> ( C e. ran ( x e. D |-> B ) <-> E. x e. D C = B ) )
14 2 13 syl 
 |-  ( ph -> ( C e. ran ( x e. D |-> B ) <-> E. x e. D C = B ) )
15 11 14 bitrd 
 |-  ( ph -> ( C e. ran ( F |` D ) <-> E. x e. D C = B ) )
16 5 15 bitrid 
 |-  ( ph -> ( C e. ( F " D ) <-> E. x e. D C = B ) )