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 𝐹 ) → ( 𝐹 “ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 { ( 𝐹 ‘ 𝑥 ) } )