| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-suc |
|- suc A = ( A u. { A } ) |
| 2 |
1
|
ineq2i |
|- ( B i^i suc A ) = ( B i^i ( A u. { A } ) ) |
| 3 |
|
indi |
|- ( B i^i ( A u. { A } ) ) = ( ( B i^i A ) u. ( B i^i { A } ) ) |
| 4 |
2 3
|
eqtri |
|- ( B i^i suc A ) = ( ( B i^i A ) u. ( B i^i { A } ) ) |
| 5 |
|
disjsn |
|- ( ( B i^i { A } ) = (/) <-> -. A e. B ) |
| 6 |
5
|
biimpri |
|- ( -. A e. B -> ( B i^i { A } ) = (/) ) |
| 7 |
6
|
uneq2d |
|- ( -. A e. B -> ( ( B i^i A ) u. ( B i^i { A } ) ) = ( ( B i^i A ) u. (/) ) ) |
| 8 |
|
un0 |
|- ( ( B i^i A ) u. (/) ) = ( B i^i A ) |
| 9 |
7 8
|
eqtrdi |
|- ( -. A e. B -> ( ( B i^i A ) u. ( B i^i { A } ) ) = ( B i^i A ) ) |
| 10 |
4 9
|
eqtrid |
|- ( -. A e. B -> ( B i^i suc A ) = ( B i^i A ) ) |