Step |
Hyp |
Ref |
Expression |
1 |
|
disj1 |
|- ( ( [ A ] R i^i [ B ] R ) = (/) <-> A. x ( x e. [ A ] R -> -. x e. [ B ] R ) ) |
2 |
|
elecg |
|- ( ( x e. _V /\ A e. V ) -> ( x e. [ A ] R <-> A R x ) ) |
3 |
2
|
el2v1 |
|- ( A e. V -> ( x e. [ A ] R <-> A R x ) ) |
4 |
3
|
adantr |
|- ( ( A e. V /\ B e. W ) -> ( x e. [ A ] R <-> A R x ) ) |
5 |
|
elecALTV |
|- ( ( B e. W /\ x e. _V ) -> ( x e. [ B ] R <-> B R x ) ) |
6 |
5
|
elvd |
|- ( B e. W -> ( x e. [ B ] R <-> B R x ) ) |
7 |
6
|
adantl |
|- ( ( A e. V /\ B e. W ) -> ( x e. [ B ] R <-> B R x ) ) |
8 |
7
|
notbid |
|- ( ( A e. V /\ B e. W ) -> ( -. x e. [ B ] R <-> -. B R x ) ) |
9 |
4 8
|
imbi12d |
|- ( ( A e. V /\ B e. W ) -> ( ( x e. [ A ] R -> -. x e. [ B ] R ) <-> ( A R x -> -. B R x ) ) ) |
10 |
9
|
albidv |
|- ( ( A e. V /\ B e. W ) -> ( A. x ( x e. [ A ] R -> -. x e. [ B ] R ) <-> A. x ( A R x -> -. B R x ) ) ) |
11 |
1 10
|
syl5bb |
|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) = (/) <-> A. x ( A R x -> -. B R x ) ) ) |