# 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 𝑥 𝐴
funimass4f.2 𝑥 𝐵
funimass4f.3 𝑥 𝐹
Assertion funimass4f ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) )

### Proof

Step Hyp Ref Expression
1 funimass4f.1 𝑥 𝐴
2 funimass4f.2 𝑥 𝐵
3 funimass4f.3 𝑥 𝐹
4 3 nffun 𝑥 Fun 𝐹
5 3 nfdm 𝑥 dom 𝐹
6 1 5 nfss 𝑥 𝐴 ⊆ dom 𝐹
7 4 6 nfan 𝑥 ( Fun 𝐹𝐴 ⊆ dom 𝐹 )
8 3 1 nfima 𝑥 ( 𝐹𝐴 )
9 8 2 nfss 𝑥 ( 𝐹𝐴 ) ⊆ 𝐵
10 7 9 nfan 𝑥 ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ ( 𝐹𝐴 ) ⊆ 𝐵 )
11 funfvima2 ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝑥𝐴 → ( 𝐹𝑥 ) ∈ ( 𝐹𝐴 ) ) )
12 ssel ( ( 𝐹𝐴 ) ⊆ 𝐵 → ( ( 𝐹𝑥 ) ∈ ( 𝐹𝐴 ) → ( 𝐹𝑥 ) ∈ 𝐵 ) )
13 11 12 sylan9 ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ ( 𝐹𝐴 ) ⊆ 𝐵 ) → ( 𝑥𝐴 → ( 𝐹𝑥 ) ∈ 𝐵 ) )
14 10 13 ralrimi ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ ( 𝐹𝐴 ) ⊆ 𝐵 ) → ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 )
15 1 3 dfimafnf ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } )
16 15 adantr ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } )
17 2 abrexss ( ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } ⊆ 𝐵 )
18 17 adantl ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) → { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } ⊆ 𝐵 )
19 16 18 eqsstrd ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) → ( 𝐹𝐴 ) ⊆ 𝐵 )
20 14 19 impbida ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ 𝐵 ) )