Step |
Hyp |
Ref |
Expression |
1 |
|
df-br |
|- ( A _E B <-> <. A , B >. e. _E ) |
2 |
|
0nelopab |
|- -. (/) e. { <. x , y >. | x e. y } |
3 |
|
df-eprel |
|- _E = { <. x , y >. | x e. y } |
4 |
3
|
eqcomi |
|- { <. x , y >. | x e. y } = _E |
5 |
4
|
eleq2i |
|- ( (/) e. { <. x , y >. | x e. y } <-> (/) e. _E ) |
6 |
2 5
|
mtbi |
|- -. (/) e. _E |
7 |
|
eleq1 |
|- ( <. A , B >. = (/) -> ( <. A , B >. e. _E <-> (/) e. _E ) ) |
8 |
6 7
|
mtbiri |
|- ( <. A , B >. = (/) -> -. <. A , B >. e. _E ) |
9 |
8
|
con2i |
|- ( <. A , B >. e. _E -> -. <. A , B >. = (/) ) |
10 |
|
opprc1 |
|- ( -. A e. _V -> <. A , B >. = (/) ) |
11 |
9 10
|
nsyl2 |
|- ( <. A , B >. e. _E -> A e. _V ) |
12 |
1 11
|
sylbi |
|- ( A _E B -> A e. _V ) |
13 |
12
|
a1i |
|- ( B e. V -> ( A _E B -> A e. _V ) ) |
14 |
|
elex |
|- ( A e. B -> A e. _V ) |
15 |
14
|
a1i |
|- ( B e. V -> ( A e. B -> A e. _V ) ) |
16 |
|
eleq12 |
|- ( ( x = A /\ y = B ) -> ( x e. y <-> A e. B ) ) |
17 |
16 3
|
brabga |
|- ( ( A e. _V /\ B e. V ) -> ( A _E B <-> A e. B ) ) |
18 |
17
|
expcom |
|- ( B e. V -> ( A e. _V -> ( A _E B <-> A e. B ) ) ) |
19 |
13 15 18
|
pm5.21ndd |
|- ( B e. V -> ( A _E B <-> A e. B ) ) |