Step |
Hyp |
Ref |
Expression |
1 |
|
treq |
|- ( z = w -> ( Tr z <-> Tr w ) ) |
2 |
|
neeq1 |
|- ( z = w -> ( z =/= (/) <-> w =/= (/) ) ) |
3 |
|
eleq2 |
|- ( z = w -> ( U. x e. z <-> U. x e. w ) ) |
4 |
|
eleq2 |
|- ( z = w -> ( ~P x e. z <-> ~P x e. w ) ) |
5 |
|
eleq2 |
|- ( z = w -> ( { x , y } e. z <-> { x , y } e. w ) ) |
6 |
5
|
raleqbi1dv |
|- ( z = w -> ( A. y e. z { x , y } e. z <-> A. y e. w { x , y } e. w ) ) |
7 |
3 4 6
|
3anbi123d |
|- ( z = w -> ( ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) <-> ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) ) |
8 |
7
|
raleqbi1dv |
|- ( z = w -> ( A. x e. z ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) <-> A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) ) |
9 |
1 2 8
|
3anbi123d |
|- ( z = w -> ( ( Tr z /\ z =/= (/) /\ A. x e. z ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) ) <-> ( Tr w /\ w =/= (/) /\ A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) ) ) |
10 |
|
treq |
|- ( w = U -> ( Tr w <-> Tr U ) ) |
11 |
|
neeq1 |
|- ( w = U -> ( w =/= (/) <-> U =/= (/) ) ) |
12 |
|
eleq2 |
|- ( w = U -> ( U. x e. w <-> U. x e. U ) ) |
13 |
|
eleq2 |
|- ( w = U -> ( ~P x e. w <-> ~P x e. U ) ) |
14 |
|
eleq2 |
|- ( w = U -> ( { x , y } e. w <-> { x , y } e. U ) ) |
15 |
14
|
raleqbi1dv |
|- ( w = U -> ( A. y e. w { x , y } e. w <-> A. y e. U { x , y } e. U ) ) |
16 |
12 13 15
|
3anbi123d |
|- ( w = U -> ( ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) <-> ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) |
17 |
16
|
raleqbi1dv |
|- ( w = U -> ( A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) <-> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) |
18 |
10 11 17
|
3anbi123d |
|- ( w = U -> ( ( Tr w /\ w =/= (/) /\ A. x e. w ( U. x e. w /\ ~P x e. w /\ A. y e. w { x , y } e. w ) ) <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) ) |
19 |
|
df-wun |
|- WUni = { z | ( Tr z /\ z =/= (/) /\ A. x e. z ( U. x e. z /\ ~P x e. z /\ A. y e. z { x , y } e. z ) ) } |
20 |
9 18 19
|
elab2gw |
|- ( U e. V -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) ) |