Step |
Hyp |
Ref |
Expression |
1 |
|
notzfaus.1 |
|- A = { (/) } |
2 |
|
notzfaus.2 |
|- ( ph <-> -. x e. y ) |
3 |
|
0ex |
|- (/) e. _V |
4 |
3
|
snnz |
|- { (/) } =/= (/) |
5 |
1 4
|
eqnetri |
|- A =/= (/) |
6 |
|
n0 |
|- ( A =/= (/) <-> E. x x e. A ) |
7 |
5 6
|
mpbi |
|- E. x x e. A |
8 |
|
pm5.19 |
|- -. ( x e. y <-> -. x e. y ) |
9 |
|
ibar |
|- ( x e. A -> ( ph <-> ( x e. A /\ ph ) ) ) |
10 |
9 2
|
bitr3di |
|- ( x e. A -> ( ( x e. A /\ ph ) <-> -. x e. y ) ) |
11 |
10
|
bibi2d |
|- ( x e. A -> ( ( x e. y <-> ( x e. A /\ ph ) ) <-> ( x e. y <-> -. x e. y ) ) ) |
12 |
8 11
|
mtbiri |
|- ( x e. A -> -. ( x e. y <-> ( x e. A /\ ph ) ) ) |
13 |
7 12
|
eximii |
|- E. x -. ( x e. y <-> ( x e. A /\ ph ) ) |
14 |
|
exnal |
|- ( E. x -. ( x e. y <-> ( x e. A /\ ph ) ) <-> -. A. x ( x e. y <-> ( x e. A /\ ph ) ) ) |
15 |
13 14
|
mpbi |
|- -. A. x ( x e. y <-> ( x e. A /\ ph ) ) |
16 |
15
|
nex |
|- -. E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) |