Step |
Hyp |
Ref |
Expression |
1 |
|
df-iota |
|- ( iota x ph ) = U. { y | { x | ph } = { y } } |
2 |
|
abeq1 |
|- ( { y | { x | ph } = { y } } = U. { z | E. w ( z = { x | ph } /\ z = { w } ) } <-> A. y ( { x | ph } = { y } <-> y e. U. { z | E. w ( z = { x | ph } /\ z = { w } ) } ) ) |
3 |
|
exdistr |
|- ( E. z E. w ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) <-> E. z ( y e. z /\ E. w ( z = { x | ph } /\ z = { w } ) ) ) |
4 |
|
vex |
|- y e. _V |
5 |
|
sneq |
|- ( w = y -> { w } = { y } ) |
6 |
5
|
eqeq2d |
|- ( w = y -> ( { x | ph } = { w } <-> { x | ph } = { y } ) ) |
7 |
4 6
|
ceqsexv |
|- ( E. w ( w = y /\ { x | ph } = { w } ) <-> { x | ph } = { y } ) |
8 |
|
snex |
|- { w } e. _V |
9 |
|
eqeq1 |
|- ( z = { w } -> ( z = { x | ph } <-> { w } = { x | ph } ) ) |
10 |
|
eleq2 |
|- ( z = { w } -> ( y e. z <-> y e. { w } ) ) |
11 |
9 10
|
anbi12d |
|- ( z = { w } -> ( ( z = { x | ph } /\ y e. z ) <-> ( { w } = { x | ph } /\ y e. { w } ) ) ) |
12 |
|
eqcom |
|- ( { w } = { x | ph } <-> { x | ph } = { w } ) |
13 |
|
velsn |
|- ( y e. { w } <-> y = w ) |
14 |
|
equcom |
|- ( y = w <-> w = y ) |
15 |
13 14
|
bitri |
|- ( y e. { w } <-> w = y ) |
16 |
12 15
|
anbi12ci |
|- ( ( { w } = { x | ph } /\ y e. { w } ) <-> ( w = y /\ { x | ph } = { w } ) ) |
17 |
11 16
|
bitrdi |
|- ( z = { w } -> ( ( z = { x | ph } /\ y e. z ) <-> ( w = y /\ { x | ph } = { w } ) ) ) |
18 |
8 17
|
ceqsexv |
|- ( E. z ( z = { w } /\ ( z = { x | ph } /\ y e. z ) ) <-> ( w = y /\ { x | ph } = { w } ) ) |
19 |
|
an13 |
|- ( ( z = { w } /\ ( z = { x | ph } /\ y e. z ) ) <-> ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
20 |
19
|
exbii |
|- ( E. z ( z = { w } /\ ( z = { x | ph } /\ y e. z ) ) <-> E. z ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
21 |
18 20
|
bitr3i |
|- ( ( w = y /\ { x | ph } = { w } ) <-> E. z ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
22 |
21
|
exbii |
|- ( E. w ( w = y /\ { x | ph } = { w } ) <-> E. w E. z ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
23 |
7 22
|
bitr3i |
|- ( { x | ph } = { y } <-> E. w E. z ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
24 |
|
excom |
|- ( E. w E. z ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) <-> E. z E. w ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
25 |
23 24
|
bitri |
|- ( { x | ph } = { y } <-> E. z E. w ( y e. z /\ ( z = { x | ph } /\ z = { w } ) ) ) |
26 |
|
eluniab |
|- ( y e. U. { z | E. w ( z = { x | ph } /\ z = { w } ) } <-> E. z ( y e. z /\ E. w ( z = { x | ph } /\ z = { w } ) ) ) |
27 |
3 25 26
|
3bitr4i |
|- ( { x | ph } = { y } <-> y e. U. { z | E. w ( z = { x | ph } /\ z = { w } ) } ) |
28 |
2 27
|
mpgbir |
|- { y | { x | ph } = { y } } = U. { z | E. w ( z = { x | ph } /\ z = { w } ) } |
29 |
|
df-sn |
|- { { x | ph } } = { z | z = { x | ph } } |
30 |
|
dfsingles2 |
|- Singletons = { z | E. w z = { w } } |
31 |
29 30
|
ineq12i |
|- ( { { x | ph } } i^i Singletons ) = ( { z | z = { x | ph } } i^i { z | E. w z = { w } } ) |
32 |
|
inab |
|- ( { z | z = { x | ph } } i^i { z | E. w z = { w } } ) = { z | ( z = { x | ph } /\ E. w z = { w } ) } |
33 |
|
19.42v |
|- ( E. w ( z = { x | ph } /\ z = { w } ) <-> ( z = { x | ph } /\ E. w z = { w } ) ) |
34 |
33
|
bicomi |
|- ( ( z = { x | ph } /\ E. w z = { w } ) <-> E. w ( z = { x | ph } /\ z = { w } ) ) |
35 |
34
|
abbii |
|- { z | ( z = { x | ph } /\ E. w z = { w } ) } = { z | E. w ( z = { x | ph } /\ z = { w } ) } |
36 |
32 35
|
eqtri |
|- ( { z | z = { x | ph } } i^i { z | E. w z = { w } } ) = { z | E. w ( z = { x | ph } /\ z = { w } ) } |
37 |
31 36
|
eqtri |
|- ( { { x | ph } } i^i Singletons ) = { z | E. w ( z = { x | ph } /\ z = { w } ) } |
38 |
37
|
unieqi |
|- U. ( { { x | ph } } i^i Singletons ) = U. { z | E. w ( z = { x | ph } /\ z = { w } ) } |
39 |
28 38
|
eqtr4i |
|- { y | { x | ph } = { y } } = U. ( { { x | ph } } i^i Singletons ) |
40 |
39
|
unieqi |
|- U. { y | { x | ph } = { y } } = U. U. ( { { x | ph } } i^i Singletons ) |
41 |
1 40
|
eqtri |
|- ( iota x ph ) = U. U. ( { { x | ph } } i^i Singletons ) |