Step |
Hyp |
Ref |
Expression |
1 |
|
dfrab3 |
|- { x e. B | ph } = ( B i^i { x | ph } ) |
2 |
1
|
ineq2i |
|- ( A i^i { x e. B | ph } ) = ( A i^i ( B i^i { x | ph } ) ) |
3 |
|
dfrab3 |
|- { x e. A | ph } = ( A i^i { x | ph } ) |
4 |
3
|
ineq2i |
|- ( B i^i { x e. A | ph } ) = ( B i^i ( A i^i { x | ph } ) ) |
5 |
|
incom |
|- ( { x e. A | ph } i^i B ) = ( B i^i { x e. A | ph } ) |
6 |
|
in12 |
|- ( A i^i ( B i^i { x | ph } ) ) = ( B i^i ( A i^i { x | ph } ) ) |
7 |
4 5 6
|
3eqtr4i |
|- ( { x e. A | ph } i^i B ) = ( A i^i ( B i^i { x | ph } ) ) |
8 |
2 7
|
eqtr4i |
|- ( A i^i { x e. B | ph } ) = ( { x e. A | ph } i^i B ) |