Step |
Hyp |
Ref |
Expression |
1 |
|
dfdif2 |
|- ( z \ U. ( x \ { z } ) ) = { v e. z | -. v e. U. ( x \ { z } ) } |
2 |
|
dfnul3 |
|- (/) = { v e. z | -. v e. z } |
3 |
2
|
uneq2i |
|- ( { v e. z | -. v e. U. ( x \ { z } ) } u. (/) ) = ( { v e. z | -. v e. U. ( x \ { z } ) } u. { v e. z | -. v e. z } ) |
4 |
|
un0 |
|- ( { v e. z | -. v e. U. ( x \ { z } ) } u. (/) ) = { v e. z | -. v e. U. ( x \ { z } ) } |
5 |
|
unrab |
|- ( { v e. z | -. v e. U. ( x \ { z } ) } u. { v e. z | -. v e. z } ) = { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) } |
6 |
3 4 5
|
3eqtr3i |
|- { v e. z | -. v e. U. ( x \ { z } ) } = { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) } |
7 |
|
ianor |
|- ( -. ( v e. U. ( x \ { z } ) /\ v e. z ) <-> ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) ) |
8 |
|
eluni |
|- ( v e. U. ( x \ { z } ) <-> E. w ( v e. w /\ w e. ( x \ { z } ) ) ) |
9 |
8
|
anbi1i |
|- ( ( v e. U. ( x \ { z } ) /\ v e. z ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
10 |
|
df-rex |
|- ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> E. w ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) ) |
11 |
|
elin |
|- ( v e. ( z i^i w ) <-> ( v e. z /\ v e. w ) ) |
12 |
11
|
anbi2i |
|- ( ( z =/= w /\ v e. ( z i^i w ) ) <-> ( z =/= w /\ ( v e. z /\ v e. w ) ) ) |
13 |
|
df-an |
|- ( ( z =/= w /\ v e. ( z i^i w ) ) <-> -. ( z =/= w -> -. v e. ( z i^i w ) ) ) |
14 |
12 13
|
bitr3i |
|- ( ( z =/= w /\ ( v e. z /\ v e. w ) ) <-> -. ( z =/= w -> -. v e. ( z i^i w ) ) ) |
15 |
14
|
anbi2i |
|- ( ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) <-> ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) ) |
16 |
|
eldifsn |
|- ( w e. ( x \ { z } ) <-> ( w e. x /\ w =/= z ) ) |
17 |
|
necom |
|- ( w =/= z <-> z =/= w ) |
18 |
17
|
anbi2i |
|- ( ( w e. x /\ w =/= z ) <-> ( w e. x /\ z =/= w ) ) |
19 |
16 18
|
bitri |
|- ( w e. ( x \ { z } ) <-> ( w e. x /\ z =/= w ) ) |
20 |
19
|
anbi2i |
|- ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( ( v e. w /\ v e. z ) /\ ( w e. x /\ z =/= w ) ) ) |
21 |
|
ancom |
|- ( ( v e. w /\ v e. z ) <-> ( v e. z /\ v e. w ) ) |
22 |
21
|
anbi2ci |
|- ( ( ( v e. w /\ v e. z ) /\ ( w e. x /\ z =/= w ) ) <-> ( ( w e. x /\ z =/= w ) /\ ( v e. z /\ v e. w ) ) ) |
23 |
|
anass |
|- ( ( ( w e. x /\ z =/= w ) /\ ( v e. z /\ v e. w ) ) <-> ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) ) |
24 |
20 22 23
|
3bitri |
|- ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) ) |
25 |
|
an32 |
|- ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
26 |
24 25
|
bitr3i |
|- ( ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
27 |
15 26
|
bitr3i |
|- ( ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
28 |
27
|
exbii |
|- ( E. w ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) <-> E. w ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
29 |
|
19.41v |
|- ( E. w ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
30 |
10 28 29
|
3bitri |
|- ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) ) |
31 |
|
rexnal |
|- ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) |
32 |
9 30 31
|
3bitr2ri |
|- ( -. A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> ( v e. U. ( x \ { z } ) /\ v e. z ) ) |
33 |
32
|
con1bii |
|- ( -. ( v e. U. ( x \ { z } ) /\ v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) |
34 |
7 33
|
bitr3i |
|- ( ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) |
35 |
34
|
rabbii |
|- { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) } = { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } |
36 |
1 6 35
|
3eqtri |
|- ( z \ U. ( x \ { z } ) ) = { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } |
37 |
36
|
neeq1i |
|- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } =/= (/) ) |
38 |
|
rabn0 |
|- ( { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) |
39 |
37 38
|
bitri |
|- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) |