Metamath Proof Explorer


Theorem dfimafn

Description: Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion dfimafn ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 } )

Proof

Step Hyp Ref Expression
1 dfima2 ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝑥 𝐹 𝑦 }
2 ssel ( 𝐴 ⊆ dom 𝐹 → ( 𝑥𝐴𝑥 ∈ dom 𝐹 ) )
3 funbrfvb ( ( Fun 𝐹𝑥 ∈ dom 𝐹 ) → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) )
4 3 ex ( Fun 𝐹 → ( 𝑥 ∈ dom 𝐹 → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) ) )
5 2 4 syl9r ( Fun 𝐹 → ( 𝐴 ⊆ dom 𝐹 → ( 𝑥𝐴 → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) ) ) )
6 5 imp31 ( ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) ∧ 𝑥𝐴 ) → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) )
7 6 rexbidva ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 ↔ ∃ 𝑥𝐴 𝑥 𝐹 𝑦 ) )
8 7 abbidv ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → { 𝑦 ∣ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑥𝐴 𝑥 𝐹 𝑦 } )
9 1 8 eqtr4id ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 } )