Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
|- ( A =/= (/) <-> E. x x e. A ) |
2 |
1
|
biimpi |
|- ( A =/= (/) -> E. x x e. A ) |
3 |
2
|
anim2i |
|- ( ( A e. V /\ A =/= (/) ) -> ( A e. V /\ E. x x e. A ) ) |
4 |
|
zfregcl |
|- ( A e. V -> ( E. x x e. A -> E. x e. A A. y e. x -. y e. A ) ) |
5 |
4
|
imp |
|- ( ( A e. V /\ E. x x e. A ) -> E. x e. A A. y e. x -. y e. A ) |
6 |
|
disj |
|- ( ( x i^i A ) = (/) <-> A. y e. x -. y e. A ) |
7 |
6
|
rexbii |
|- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A A. y e. x -. y e. A ) |
8 |
7
|
biimpri |
|- ( E. x e. A A. y e. x -. y e. A -> E. x e. A ( x i^i A ) = (/) ) |
9 |
3 5 8
|
3syl |
|- ( ( A e. V /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) ) |