Theorem funimaexg

Description: Axiom of Replacement using abbreviations. Axiom 39(vi) of Quine p. 284. Compare Exercise 9 of TakeutiZaring p. 29. (Contributed by NM, 10-Sep-2006)

	Ref	Expression
Assertion	funimaexg	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 “ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		imaeq2	⊢ ( 𝑤 = 𝐵 → ( 𝐴 “ 𝑤 ) = ( 𝐴 “ 𝐵 ) )
2	1	eleq1d	⊢ ( 𝑤 = 𝐵 → ( ( 𝐴 “ 𝑤 ) ∈ V ↔ ( 𝐴 “ 𝐵 ) ∈ V ) )
3	2	imbi2d	⊢ ( 𝑤 = 𝐵 → ( ( Fun 𝐴 → ( 𝐴 “ 𝑤 ) ∈ V ) ↔ ( Fun 𝐴 → ( 𝐴 “ 𝐵 ) ∈ V ) ) )
4		dffun5	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) ) )
5		nfv	⊢ Ⅎ 𝑧 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴
6	5	axrep4	⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
7		isset	⊢ ( ( 𝐴 “ 𝑤 ) ∈ V ↔ ∃ 𝑧 𝑧 = ( 𝐴 “ 𝑤 ) )
8		dfima3	⊢ ( 𝐴 “ 𝑤 ) = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) }
9	8	eqeq2i	⊢ ( 𝑧 = ( 𝐴 “ 𝑤 ) ↔ 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } )
10		abeq2	⊢ ( 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
11	9 10	bitri	⊢ ( 𝑧 = ( 𝐴 “ 𝑤 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
12	11	exbii	⊢ ( ∃ 𝑧 𝑧 = ( 𝐴 “ 𝑤 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
13	7 12	bitri	⊢ ( ( 𝐴 “ 𝑤 ) ∈ V ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑤 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) )
14	6 13	sylibr	⊢ ( ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 = 𝑧 ) → ( 𝐴 “ 𝑤 ) ∈ V )
15	4 14	simplbiim	⊢ ( Fun 𝐴 → ( 𝐴 “ 𝑤 ) ∈ V )
16	3 15	vtoclg	⊢ ( 𝐵 ∈ 𝐶 → ( Fun 𝐴 → ( 𝐴 “ 𝐵 ) ∈ V ) )
17	16	impcom	⊢ ( ( Fun 𝐴 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 “ 𝐵 ) ∈ V )