Metamath Proof Explorer


Theorem dfimafnf

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006) (Revised by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses dfimafnf.1 𝑥 𝐴
dfimafnf.2 𝑥 𝐹
Assertion dfimafnf ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } )

Proof

Step Hyp Ref Expression
1 dfimafnf.1 𝑥 𝐴
2 dfimafnf.2 𝑥 𝐹
3 ssel ( 𝐴 ⊆ dom 𝐹 → ( 𝑧𝐴𝑧 ∈ dom 𝐹 ) )
4 eqcom ( ( 𝐹𝑧 ) = 𝑦𝑦 = ( 𝐹𝑧 ) )
5 funbrfvb ( ( Fun 𝐹𝑧 ∈ dom 𝐹 ) → ( ( 𝐹𝑧 ) = 𝑦𝑧 𝐹 𝑦 ) )
6 4 5 bitr3id ( ( Fun 𝐹𝑧 ∈ dom 𝐹 ) → ( 𝑦 = ( 𝐹𝑧 ) ↔ 𝑧 𝐹 𝑦 ) )
7 6 ex ( Fun 𝐹 → ( 𝑧 ∈ dom 𝐹 → ( 𝑦 = ( 𝐹𝑧 ) ↔ 𝑧 𝐹 𝑦 ) ) )
8 3 7 syl9r ( Fun 𝐹 → ( 𝐴 ⊆ dom 𝐹 → ( 𝑧𝐴 → ( 𝑦 = ( 𝐹𝑧 ) ↔ 𝑧 𝐹 𝑦 ) ) ) )
9 8 imp31 ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ 𝑧𝐴 ) → ( 𝑦 = ( 𝐹𝑧 ) ↔ 𝑧 𝐹 𝑦 ) )
10 9 rexbidva ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ∃ 𝑧𝐴 𝑦 = ( 𝐹𝑧 ) ↔ ∃ 𝑧𝐴 𝑧 𝐹 𝑦 ) )
11 10 abbidv ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → { 𝑦 ∣ ∃ 𝑧𝐴 𝑦 = ( 𝐹𝑧 ) } = { 𝑦 ∣ ∃ 𝑧𝐴 𝑧 𝐹 𝑦 } )
12 dfima2 ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑧𝐴 𝑧 𝐹 𝑦 }
13 11 12 syl6reqr ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑧𝐴 𝑦 = ( 𝐹𝑧 ) } )
14 nfcv 𝑧 𝐴
15 nfcv 𝑥 𝑧
16 2 15 nffv 𝑥 ( 𝐹𝑧 )
17 16 nfeq2 𝑥 𝑦 = ( 𝐹𝑧 )
18 nfv 𝑧 𝑦 = ( 𝐹𝑥 )
19 fveq2 ( 𝑧 = 𝑥 → ( 𝐹𝑧 ) = ( 𝐹𝑥 ) )
20 19 eqeq2d ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝐹𝑧 ) ↔ 𝑦 = ( 𝐹𝑥 ) ) )
21 14 1 17 18 20 cbvrexfw ( ∃ 𝑧𝐴 𝑦 = ( 𝐹𝑧 ) ↔ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) )
22 21 abbii { 𝑦 ∣ ∃ 𝑧𝐴 𝑦 = ( 𝐹𝑧 ) } = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) }
23 13 22 syl6eq ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) } )