Step |
Hyp |
Ref |
Expression |
1 |
|
nfv |
|- F/ z E. x e. A ph |
2 |
|
nfcv |
|- F/_ y A |
3 |
|
nfs1v |
|- F/ y [ z / y ] ph |
4 |
2 3
|
nfrex |
|- F/ y E. x e. A [ z / y ] ph |
5 |
|
sbequ12 |
|- ( y = z -> ( ph <-> [ z / y ] ph ) ) |
6 |
5
|
rexbidv |
|- ( y = z -> ( E. x e. A ph <-> E. x e. A [ z / y ] ph ) ) |
7 |
1 4 6
|
cbvabw |
|- { y | E. x e. A ph } = { z | E. x e. A [ z / y ] ph } |
8 |
|
df-clab |
|- ( z e. { y | ph } <-> [ z / y ] ph ) |
9 |
8
|
rexbii |
|- ( E. x e. A z e. { y | ph } <-> E. x e. A [ z / y ] ph ) |
10 |
9
|
abbii |
|- { z | E. x e. A z e. { y | ph } } = { z | E. x e. A [ z / y ] ph } |
11 |
7 10
|
eqtr4i |
|- { y | E. x e. A ph } = { z | E. x e. A z e. { y | ph } } |
12 |
|
df-iun |
|- U_ x e. A { y | ph } = { z | E. x e. A z e. { y | ph } } |
13 |
|
iunexg |
|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> U_ x e. A { y | ph } e. _V ) |
14 |
12 13
|
eqeltrrid |
|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { z | E. x e. A z e. { y | ph } } e. _V ) |
15 |
11 14
|
eqeltrid |
|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { y | E. x e. A ph } e. _V ) |