Step |
Hyp |
Ref |
Expression |
0 |
|
cwun |
|- WUni |
1 |
|
vu |
|- u |
2 |
1
|
cv |
|- u |
3 |
2
|
wtr |
|- Tr u |
4 |
|
c0 |
|- (/) |
5 |
2 4
|
wne |
|- u =/= (/) |
6 |
|
vx |
|- x |
7 |
6
|
cv |
|- x |
8 |
7
|
cuni |
|- U. x |
9 |
8 2
|
wcel |
|- U. x e. u |
10 |
7
|
cpw |
|- ~P x |
11 |
10 2
|
wcel |
|- ~P x e. u |
12 |
|
vy |
|- y |
13 |
12
|
cv |
|- y |
14 |
7 13
|
cpr |
|- { x , y } |
15 |
14 2
|
wcel |
|- { x , y } e. u |
16 |
15 12 2
|
wral |
|- A. y e. u { x , y } e. u |
17 |
9 11 16
|
w3a |
|- ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) |
18 |
17 6 2
|
wral |
|- A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) |
19 |
3 5 18
|
w3a |
|- ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) |
20 |
19 1
|
cab |
|- { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) } |
21 |
0 20
|
wceq |
|- WUni = { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) } |