| 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 |
|
uncom |
|- ( ( B i^i A ) u. ( B i^i { A } ) ) = ( ( B i^i { A } ) u. ( B i^i A ) ) |
| 5 |
2 3 4
|
3eqtri |
|- ( B i^i suc A ) = ( ( B i^i { A } ) u. ( B i^i A ) ) |
| 6 |
|
snssi |
|- ( A e. B -> { A } C_ B ) |
| 7 |
|
sseqin2 |
|- ( { A } C_ B <-> ( B i^i { A } ) = { A } ) |
| 8 |
6 7
|
sylib |
|- ( A e. B -> ( B i^i { A } ) = { A } ) |
| 9 |
8
|
uneq1d |
|- ( A e. B -> ( ( B i^i { A } ) u. ( B i^i A ) ) = ( { A } u. ( B i^i A ) ) ) |
| 10 |
5 9
|
eqtrid |
|- ( A e. B -> ( B i^i suc A ) = ( { A } u. ( B i^i A ) ) ) |