Step |
Hyp |
Ref |
Expression |
1 |
|
19.42v |
|- ( E. y ( x e. z /\ ph ) <-> ( x e. z /\ E. y ph ) ) |
2 |
1
|
abbii |
|- { x | E. y ( x e. z /\ ph ) } = { x | ( x e. z /\ E. y ph ) } |
3 |
|
dmopab |
|- dom { <. x , y >. | ( x e. z /\ ph ) } = { x | E. y ( x e. z /\ ph ) } |
4 |
|
df-rab |
|- { x e. z | E. y ph } = { x | ( x e. z /\ E. y ph ) } |
5 |
2 3 4
|
3eqtr4i |
|- dom { <. x , y >. | ( x e. z /\ ph ) } = { x e. z | E. y ph } |
6 |
|
euex |
|- ( E! y ph -> E. y ph ) |
7 |
6
|
ralimi |
|- ( A. x e. z E! y ph -> A. x e. z E. y ph ) |
8 |
|
rabid2 |
|- ( z = { x e. z | E. y ph } <-> A. x e. z E. y ph ) |
9 |
7 8
|
sylibr |
|- ( A. x e. z E! y ph -> z = { x e. z | E. y ph } ) |
10 |
5 9
|
eqtr4id |
|- ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } = z ) |
11 |
|
vex |
|- z e. _V |
12 |
10 11
|
eqeltrdi |
|- ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } e. _V ) |
13 |
|
eumo |
|- ( E! y ph -> E* y ph ) |
14 |
13
|
imim2i |
|- ( ( x e. z -> E! y ph ) -> ( x e. z -> E* y ph ) ) |
15 |
|
moanimv |
|- ( E* y ( x e. z /\ ph ) <-> ( x e. z -> E* y ph ) ) |
16 |
14 15
|
sylibr |
|- ( ( x e. z -> E! y ph ) -> E* y ( x e. z /\ ph ) ) |
17 |
16
|
alimi |
|- ( A. x ( x e. z -> E! y ph ) -> A. x E* y ( x e. z /\ ph ) ) |
18 |
|
df-ral |
|- ( A. x e. z E! y ph <-> A. x ( x e. z -> E! y ph ) ) |
19 |
|
funopab |
|- ( Fun { <. x , y >. | ( x e. z /\ ph ) } <-> A. x E* y ( x e. z /\ ph ) ) |
20 |
17 18 19
|
3imtr4i |
|- ( A. x e. z E! y ph -> Fun { <. x , y >. | ( x e. z /\ ph ) } ) |
21 |
|
funrnex |
|- ( dom { <. x , y >. | ( x e. z /\ ph ) } e. _V -> ( Fun { <. x , y >. | ( x e. z /\ ph ) } -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V ) ) |
22 |
12 20 21
|
sylc |
|- ( A. x e. z E! y ph -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V ) |
23 |
|
nfra1 |
|- F/ x A. x e. z E! y ph |
24 |
10
|
eleq2d |
|- ( A. x e. z E! y ph -> ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> x e. z ) ) |
25 |
|
opabidw |
|- ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } <-> ( x e. z /\ ph ) ) |
26 |
|
vex |
|- x e. _V |
27 |
|
vex |
|- y e. _V |
28 |
26 27
|
opelrn |
|- ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } ) |
29 |
25 28
|
sylbir |
|- ( ( x e. z /\ ph ) -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } ) |
30 |
29
|
ex |
|- ( x e. z -> ( ph -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } ) ) |
31 |
30
|
impac |
|- ( ( x e. z /\ ph ) -> ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) ) |
32 |
31
|
eximi |
|- ( E. y ( x e. z /\ ph ) -> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) ) |
33 |
3
|
abeq2i |
|- ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> E. y ( x e. z /\ ph ) ) |
34 |
|
df-rex |
|- ( E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph <-> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) ) |
35 |
32 33 34
|
3imtr4i |
|- ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) |
36 |
24 35
|
syl6bir |
|- ( A. x e. z E! y ph -> ( x e. z -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) ) |
37 |
23 36
|
ralrimi |
|- ( A. x e. z E! y ph -> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) |
38 |
|
nfopab1 |
|- F/_ x { <. x , y >. | ( x e. z /\ ph ) } |
39 |
38
|
nfrn |
|- F/_ x ran { <. x , y >. | ( x e. z /\ ph ) } |
40 |
39
|
nfeq2 |
|- F/ x w = ran { <. x , y >. | ( x e. z /\ ph ) } |
41 |
|
nfcv |
|- F/_ y w |
42 |
|
nfopab2 |
|- F/_ y { <. x , y >. | ( x e. z /\ ph ) } |
43 |
42
|
nfrn |
|- F/_ y ran { <. x , y >. | ( x e. z /\ ph ) } |
44 |
41 43
|
rexeqf |
|- ( w = ran { <. x , y >. | ( x e. z /\ ph ) } -> ( E. y e. w ph <-> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) ) |
45 |
40 44
|
ralbid |
|- ( w = ran { <. x , y >. | ( x e. z /\ ph ) } -> ( A. x e. z E. y e. w ph <-> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) ) |
46 |
22 37 45
|
spcedv |
|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph ) |