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

Metamath Proof Explorer

Theorem imassmpt

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses imassmpt.1 
|- F/ x ph
imassmpt.2 
|- ( ( ph /\ x e. ( A i^i C ) ) -> B e. V )
imassmpt.3 
|- F = ( x e. A |-> B )
Assertion imassmpt 
|- ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )

Proof

Step Hyp Ref Expression
1 imassmpt.1 
 |-  F/ x ph
2 imassmpt.2 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> B e. V )
3 imassmpt.3 
 |-  F = ( x e. A |-> B )
4 df-ima 
 |-  ( F " C ) = ran ( F |` C )
5 3 reseq1i 
 |-  ( F |` C ) = ( ( x e. A |-> B ) |` C )
6 resmpt3 
 |-  ( ( x e. A |-> B ) |` C ) = ( x e. ( A i^i C ) |-> B )
7 5 6 eqtri 
 |-  ( F |` C ) = ( x e. ( A i^i C ) |-> B )
8 7 rneqi 
 |-  ran ( F |` C ) = ran ( x e. ( A i^i C ) |-> B )
9 4 8 eqtri 
 |-  ( F " C ) = ran ( x e. ( A i^i C ) |-> B )
10 9 sseq1i 
 |-  ( ( F " C ) C_ D <-> ran ( x e. ( A i^i C ) |-> B ) C_ D )
11 eqid 
 |-  ( x e. ( A i^i C ) |-> B ) = ( x e. ( A i^i C ) |-> B )
12 1 11 2 rnmptssbi 
 |-  ( ph -> ( ran ( x e. ( A i^i C ) |-> B ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )
13 10 12 bitrid 
 |-  ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )