# 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 ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {A}\left[{B}\right]\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 imaeq2 ${⊢}{w}={B}\to {A}\left[{w}\right]={A}\left[{B}\right]$
2 1 eleq1d ${⊢}{w}={B}\to \left({A}\left[{w}\right]\in \mathrm{V}↔{A}\left[{B}\right]\in \mathrm{V}\right)$
3 2 imbi2d ${⊢}{w}={B}\to \left(\left(\mathrm{Fun}{A}\to {A}\left[{w}\right]\in \mathrm{V}\right)↔\left(\mathrm{Fun}{A}\to {A}\left[{B}\right]\in \mathrm{V}\right)\right)$
4 dffun5 ${⊢}\mathrm{Fun}{A}↔\left(\mathrm{Rel}{A}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)\right)$
5 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
6 5 axrep4 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right)$
7 isset ${⊢}{A}\left[{w}\right]\in \mathrm{V}↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}={A}\left[{w}\right]$
8 dfima3 ${⊢}{A}\left[{w}\right]=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right\}$
9 8 eqeq2i ${⊢}{z}={A}\left[{w}\right]↔{z}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right\}$
10 abeq2 ${⊢}{z}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right\}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right)$
11 9 10 bitri ${⊢}{z}={A}\left[{w}\right]↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right)$
12 11 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}{z}={A}\left[{w}\right]↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right)$
13 7 12 bitri ${⊢}{A}\left[{w}\right]\in \mathrm{V}↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {z}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ⟨{x},{y}⟩\in {A}\right)\right)$
14 6 13 sylibr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}\to {y}={z}\right)\to {A}\left[{w}\right]\in \mathrm{V}$
15 4 14 simplbiim ${⊢}\mathrm{Fun}{A}\to {A}\left[{w}\right]\in \mathrm{V}$
16 3 15 vtoclg ${⊢}{B}\in {C}\to \left(\mathrm{Fun}{A}\to {A}\left[{B}\right]\in \mathrm{V}\right)$
17 16 impcom ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {A}\left[{B}\right]\in \mathrm{V}$