Step |
Hyp |
Ref |
Expression |
1 |
|
dfcoss2 |
|- ,~ (/) = { <. y , z >. | E. x ( y e. [ x ] (/) /\ z e. [ x ] (/) ) } |
2 |
|
ec0 |
|- [ x ] (/) = (/) |
3 |
2
|
eleq2i |
|- ( y e. [ x ] (/) <-> y e. (/) ) |
4 |
2
|
eleq2i |
|- ( z e. [ x ] (/) <-> z e. (/) ) |
5 |
3 4
|
anbi12i |
|- ( ( y e. [ x ] (/) /\ z e. [ x ] (/) ) <-> ( y e. (/) /\ z e. (/) ) ) |
6 |
5
|
exbii |
|- ( E. x ( y e. [ x ] (/) /\ z e. [ x ] (/) ) <-> E. x ( y e. (/) /\ z e. (/) ) ) |
7 |
|
19.9v |
|- ( E. x ( y e. (/) /\ z e. (/) ) <-> ( y e. (/) /\ z e. (/) ) ) |
8 |
6 7
|
bitri |
|- ( E. x ( y e. [ x ] (/) /\ z e. [ x ] (/) ) <-> ( y e. (/) /\ z e. (/) ) ) |
9 |
8
|
opabbii |
|- { <. y , z >. | E. x ( y e. [ x ] (/) /\ z e. [ x ] (/) ) } = { <. y , z >. | ( y e. (/) /\ z e. (/) ) } |
10 |
|
prnzg |
|- ( y e. _V -> { y , z } =/= (/) ) |
11 |
10
|
elv |
|- { y , z } =/= (/) |
12 |
|
ss0b |
|- ( { y , z } C_ (/) <-> { y , z } = (/) ) |
13 |
11 12
|
nemtbir |
|- -. { y , z } C_ (/) |
14 |
|
prssg |
|- ( ( y e. _V /\ z e. _V ) -> ( ( y e. (/) /\ z e. (/) ) <-> { y , z } C_ (/) ) ) |
15 |
14
|
el2v |
|- ( ( y e. (/) /\ z e. (/) ) <-> { y , z } C_ (/) ) |
16 |
13 15
|
mtbir |
|- -. ( y e. (/) /\ z e. (/) ) |
17 |
16
|
opabf |
|- { <. y , z >. | ( y e. (/) /\ z e. (/) ) } = (/) |
18 |
1 9 17
|
3eqtri |
|- ,~ (/) = (/) |