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