Step |
Hyp |
Ref |
Expression |
1 |
|
indif2 |
|- ( E i^i ( U. S \ F ) ) = ( ( E i^i U. S ) \ F ) |
2 |
1
|
a1i |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i ( U. S \ F ) ) = ( ( E i^i U. S ) \ F ) ) |
3 |
|
elssuni |
|- ( E e. S -> E C_ U. S ) |
4 |
|
df-ss |
|- ( E C_ U. S <-> ( E i^i U. S ) = E ) |
5 |
3 4
|
sylib |
|- ( E e. S -> ( E i^i U. S ) = E ) |
6 |
5
|
difeq1d |
|- ( E e. S -> ( ( E i^i U. S ) \ F ) = ( E \ F ) ) |
7 |
6
|
3ad2ant2 |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( ( E i^i U. S ) \ F ) = ( E \ F ) ) |
8 |
2 7
|
eqtr2d |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E \ F ) = ( E i^i ( U. S \ F ) ) ) |
9 |
|
simp1 |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> S e. SAlg ) |
10 |
|
simp2 |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> E e. S ) |
11 |
|
saldifcl |
|- ( ( S e. SAlg /\ F e. S ) -> ( U. S \ F ) e. S ) |
12 |
11
|
3adant2 |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( U. S \ F ) e. S ) |
13 |
|
salincl |
|- ( ( S e. SAlg /\ E e. S /\ ( U. S \ F ) e. S ) -> ( E i^i ( U. S \ F ) ) e. S ) |
14 |
9 10 12 13
|
syl3anc |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E i^i ( U. S \ F ) ) e. S ) |
15 |
8 14
|
eqeltrd |
|- ( ( S e. SAlg /\ E e. S /\ F e. S ) -> ( E \ F ) e. S ) |