Metamath Proof Explorer

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 ⁡ A ∧ B ∈ C → A B ∈ V

Proof

Step Hyp Ref Expression
1 imaeq2 ⊢ w = B → A w = A B
2 1 eleq1d ⊢ w = B → A w ∈ V ↔ A B ∈ V
3 2 imbi2d ⊢ w = B → Fun ⁡ A → A w ∈ V ↔ Fun ⁡ A → A B ∈ V
4 dffun5 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x y ∈ A → y = z
5 nfv ⊢ Ⅎ z x y ∈ A
6 5 axrep4 ⊢ ∀ x ∃ z ∀ y x y ∈ A → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ x y ∈ A
7 isset ⊢ A w ∈ V ↔ ∃ z z = A w
8 dfima3 ⊢ A w = y | ∃ x x ∈ w ∧ x y ∈ A
9 8 eqeq2i ⊢ z = A w ↔ z = y | ∃ x x ∈ w ∧ x y ∈ A
10 abeq2 ⊢ z = y | ∃ x x ∈ w ∧ x y ∈ A ↔ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ x y ∈ A
11 9 10 bitri ⊢ z = A w ↔ ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ x y ∈ A
12 11 exbii ⊢ ∃ z z = A w ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ x y ∈ A
13 7 12 bitri ⊢ A w ∈ V ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ w ∧ x y ∈ A
14 6 13 sylibr ⊢ ∀ x ∃ z ∀ y x y ∈ A → y = z → A w ∈ V
15 4 14 simplbiim ⊢ Fun ⁡ A → A w ∈ V
16 3 15 vtoclg ⊢ B ∈ C → Fun ⁡ A → A B ∈ V
17 16 impcom ⊢ Fun ⁡ A ∧ B ∈ C → A B ∈ V