Step |
Hyp |
Ref |
Expression |
1 |
|
df-ss |
|- ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i V ) i^i ( V \ B ) ) = ( A i^i V ) ) |
2 |
|
indif2 |
|- ( ( A i^i V ) i^i ( V \ B ) ) = ( ( ( A i^i V ) i^i V ) \ B ) |
3 |
|
inss1 |
|- ( ( A i^i V ) i^i V ) C_ ( A i^i V ) |
4 |
|
ssid |
|- ( A i^i V ) C_ ( A i^i V ) |
5 |
|
inss2 |
|- ( A i^i V ) C_ V |
6 |
4 5
|
ssini |
|- ( A i^i V ) C_ ( ( A i^i V ) i^i V ) |
7 |
3 6
|
eqssi |
|- ( ( A i^i V ) i^i V ) = ( A i^i V ) |
8 |
7
|
difeq1i |
|- ( ( ( A i^i V ) i^i V ) \ B ) = ( ( A i^i V ) \ B ) |
9 |
2 8
|
eqtri |
|- ( ( A i^i V ) i^i ( V \ B ) ) = ( ( A i^i V ) \ B ) |
10 |
9
|
eqeq1i |
|- ( ( ( A i^i V ) i^i ( V \ B ) ) = ( A i^i V ) <-> ( ( A i^i V ) \ B ) = ( A i^i V ) ) |
11 |
|
eqcom |
|- ( ( ( A i^i V ) \ B ) = ( A i^i V ) <-> ( A i^i V ) = ( ( A i^i V ) \ B ) ) |
12 |
1 10 11
|
3bitri |
|- ( ( A i^i V ) C_ ( V \ B ) <-> ( A i^i V ) = ( ( A i^i V ) \ B ) ) |
13 |
|
disj3 |
|- ( ( ( A i^i V ) i^i B ) = (/) <-> ( A i^i V ) = ( ( A i^i V ) \ B ) ) |
14 |
|
in32 |
|- ( ( A i^i V ) i^i B ) = ( ( A i^i B ) i^i V ) |
15 |
14
|
eqeq1i |
|- ( ( ( A i^i V ) i^i B ) = (/) <-> ( ( A i^i B ) i^i V ) = (/) ) |
16 |
12 13 15
|
3bitr2i |
|- ( ( A i^i V ) C_ ( V \ B ) <-> ( ( A i^i B ) i^i V ) = (/) ) |