Step |
Hyp |
Ref |
Expression |
1 |
|
dfclel |
|- ( { x | ph } e. { y | ps } <-> E. z ( z = { x | ph } /\ z e. { y | ps } ) ) |
2 |
|
eliminable-veqab |
|- ( z = { x | ph } <-> A. t ( t e. z <-> [ t / x ] ph ) ) |
3 |
|
eliminable-velab |
|- ( z e. { y | ps } <-> [ z / y ] ps ) |
4 |
2 3
|
anbi12i |
|- ( ( z = { x | ph } /\ z e. { y | ps } ) <-> ( A. t ( t e. z <-> [ t / x ] ph ) /\ [ z / y ] ps ) ) |
5 |
4
|
exbii |
|- ( E. z ( z = { x | ph } /\ z e. { y | ps } ) <-> E. z ( A. t ( t e. z <-> [ t / x ] ph ) /\ [ z / y ] ps ) ) |
6 |
1 5
|
bitri |
|- ( { x | ph } e. { y | ps } <-> E. z ( A. t ( t e. z <-> [ t / x ] ph ) /\ [ z / y ] ps ) ) |