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		dfima2	⊢ ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑧 𝐹 𝑦 }
4		ssel	⊢ ( 𝐴 ⊆ dom 𝐹 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ dom 𝐹 ) )
5		eqcom	⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑧 ) )
6		funbrfvb	⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑧 𝐹 𝑦 ) )
7	5 6	bitr3id	⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) )
8	7	ex	⊢ ( Fun 𝐹 → ( 𝑧 ∈ dom 𝐹 → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) ) )
9	4 8	syl9r	⊢ ( Fun 𝐹 → ( 𝐴 ⊆ dom 𝐹 → ( 𝑧 ∈ 𝐴 → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) ) ) )
10	9	imp31	⊢ ( ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 𝐹 𝑦 ) )
11	10	rexbidva	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑧 𝐹 𝑦 ) )
12	11	abbidv	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑧 𝐹 𝑦 } )
13	3 12	eqtr4id	⊢ ( ( 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	eqtrdi	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )