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 syl5bb
 |-  ( ph -> ( ( F " C ) C_ D <-> A. x e. ( A i^i C ) B e. D ) )