# Metamath Proof Explorer

## Theorem funimass4f

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses funimass4f.1
`|- F/_ x A`
funimass4f.2
`|- F/_ x B`
funimass4f.3
`|- F/_ x F`
Assertion funimass4f
`|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )`

### Proof

Step Hyp Ref Expression
1 funimass4f.1
` |-  F/_ x A`
2 funimass4f.2
` |-  F/_ x B`
3 funimass4f.3
` |-  F/_ x F`
4 3 nffun
` |-  F/ x Fun F`
5 3 nfdm
` |-  F/_ x dom F`
6 1 5 nfss
` |-  F/ x A C_ dom F`
7 4 6 nfan
` |-  F/ x ( Fun F /\ A C_ dom F )`
8 3 1 nfima
` |-  F/_ x ( F " A )`
9 8 2 nfss
` |-  F/ x ( F " A ) C_ B`
10 7 9 nfan
` |-  F/ x ( ( Fun F /\ A C_ dom F ) /\ ( F " A ) C_ B )`
11 funfvima2
` |-  ( ( Fun F /\ A C_ dom F ) -> ( x e. A -> ( F ` x ) e. ( F " A ) ) )`
12 ssel
` |-  ( ( F " A ) C_ B -> ( ( F ` x ) e. ( F " A ) -> ( F ` x ) e. B ) )`
13 11 12 sylan9
` |-  ( ( ( Fun F /\ A C_ dom F ) /\ ( F " A ) C_ B ) -> ( x e. A -> ( F ` x ) e. B ) )`
14 10 13 ralrimi
` |-  ( ( ( Fun F /\ A C_ dom F ) /\ ( F " A ) C_ B ) -> A. x e. A ( F ` x ) e. B )`
15 1 3 dfimafnf
` |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A y = ( F ` x ) } )`
` |-  ( ( ( Fun F /\ A C_ dom F ) /\ A. x e. A ( F ` x ) e. B ) -> ( F " A ) = { y | E. x e. A y = ( F ` x ) } )`
` |-  ( A. x e. A ( F ` x ) e. B -> { y | E. x e. A y = ( F ` x ) } C_ B )`
` |-  ( ( ( Fun F /\ A C_ dom F ) /\ A. x e. A ( F ` x ) e. B ) -> { y | E. x e. A y = ( F ` x ) } C_ B )`
` |-  ( ( ( Fun F /\ A C_ dom F ) /\ A. x e. A ( F ` x ) e. B ) -> ( F " A ) C_ B )`
` |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )`