Step |
Hyp |
Ref |
Expression |
1 |
|
isfbas |
|- ( B e. A -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) ) |
2 |
|
elin |
|- ( z e. ( F i^i ~P ( x i^i y ) ) <-> ( z e. F /\ z e. ~P ( x i^i y ) ) ) |
3 |
|
velpw |
|- ( z e. ~P ( x i^i y ) <-> z C_ ( x i^i y ) ) |
4 |
3
|
anbi2i |
|- ( ( z e. F /\ z e. ~P ( x i^i y ) ) <-> ( z e. F /\ z C_ ( x i^i y ) ) ) |
5 |
2 4
|
bitri |
|- ( z e. ( F i^i ~P ( x i^i y ) ) <-> ( z e. F /\ z C_ ( x i^i y ) ) ) |
6 |
5
|
exbii |
|- ( E. z z e. ( F i^i ~P ( x i^i y ) ) <-> E. z ( z e. F /\ z C_ ( x i^i y ) ) ) |
7 |
|
n0 |
|- ( ( F i^i ~P ( x i^i y ) ) =/= (/) <-> E. z z e. ( F i^i ~P ( x i^i y ) ) ) |
8 |
|
df-rex |
|- ( E. z e. F z C_ ( x i^i y ) <-> E. z ( z e. F /\ z C_ ( x i^i y ) ) ) |
9 |
6 7 8
|
3bitr4i |
|- ( ( F i^i ~P ( x i^i y ) ) =/= (/) <-> E. z e. F z C_ ( x i^i y ) ) |
10 |
9
|
2ralbii |
|- ( A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) <-> A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) |
11 |
10
|
3anbi3i |
|- ( ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) <-> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) |
12 |
11
|
anbi2i |
|- ( ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) |
13 |
1 12
|
bitrdi |
|- ( B e. A -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) ) |