Metamath Proof Explorer


Theorem dfimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion dfimafn2 ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = 𝑥𝐴 { ( 𝐹𝑥 ) } )

Proof

Step Hyp Ref Expression
1 dfimafn ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 } )
2 iunab 𝑥𝐴 { 𝑦 ∣ ( 𝐹𝑥 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝑦 }
3 1 2 eqtr4di ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = 𝑥𝐴 { 𝑦 ∣ ( 𝐹𝑥 ) = 𝑦 } )
4 df-sn { ( 𝐹𝑥 ) } = { 𝑦𝑦 = ( 𝐹𝑥 ) }
5 eqcom ( 𝑦 = ( 𝐹𝑥 ) ↔ ( 𝐹𝑥 ) = 𝑦 )
6 5 abbii { 𝑦𝑦 = ( 𝐹𝑥 ) } = { 𝑦 ∣ ( 𝐹𝑥 ) = 𝑦 }
7 4 6 eqtri { ( 𝐹𝑥 ) } = { 𝑦 ∣ ( 𝐹𝑥 ) = 𝑦 }
8 7 a1i ( 𝑥𝐴 → { ( 𝐹𝑥 ) } = { 𝑦 ∣ ( 𝐹𝑥 ) = 𝑦 } )
9 8 iuneq2i 𝑥𝐴 { ( 𝐹𝑥 ) } = 𝑥𝐴 { 𝑦 ∣ ( 𝐹𝑥 ) = 𝑦 }
10 3 9 eqtr4di ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) = 𝑥𝐴 { ( 𝐹𝑥 ) } )