Step |
Hyp |
Ref |
Expression |
1 |
|
riotasv3d.1 |
|- F/ y ph |
2 |
|
riotasv3d.2 |
|- ( ph -> F/ y th ) |
3 |
|
riotasv3d.3 |
|- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) |
4 |
|
riotasv3d.4 |
|- ( ( ph /\ C = D ) -> ( ch <-> th ) ) |
5 |
|
riotasv3d.5 |
|- ( ph -> ( ( y e. B /\ ps ) -> ch ) ) |
6 |
|
riotasv3d.6 |
|- ( ph -> D e. A ) |
7 |
|
riotasv3d.7 |
|- ( ph -> E. y e. B ps ) |
8 |
|
elex |
|- ( A e. V -> A e. _V ) |
9 |
7
|
adantr |
|- ( ( ph /\ A e. _V ) -> E. y e. B ps ) |
10 |
|
nfv |
|- F/ y A e. _V |
11 |
5
|
imp |
|- ( ( ph /\ ( y e. B /\ ps ) ) -> ch ) |
12 |
11
|
adantrl |
|- ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> ch ) |
13 |
3 6
|
riotasvd |
|- ( ( ph /\ A e. _V ) -> ( ( y e. B /\ ps ) -> D = C ) ) |
14 |
13
|
impr |
|- ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> D = C ) |
15 |
14
|
eqcomd |
|- ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> C = D ) |
16 |
15 4
|
syldan |
|- ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> ( ch <-> th ) ) |
17 |
12 16
|
mpbid |
|- ( ( ph /\ ( A e. _V /\ ( y e. B /\ ps ) ) ) -> th ) |
18 |
17
|
exp45 |
|- ( ph -> ( A e. _V -> ( y e. B -> ( ps -> th ) ) ) ) |
19 |
1 10 18
|
ralrimd |
|- ( ph -> ( A e. _V -> A. y e. B ( ps -> th ) ) ) |
20 |
|
r19.23t |
|- ( F/ y th -> ( A. y e. B ( ps -> th ) <-> ( E. y e. B ps -> th ) ) ) |
21 |
2 20
|
syl |
|- ( ph -> ( A. y e. B ( ps -> th ) <-> ( E. y e. B ps -> th ) ) ) |
22 |
19 21
|
sylibd |
|- ( ph -> ( A e. _V -> ( E. y e. B ps -> th ) ) ) |
23 |
22
|
imp |
|- ( ( ph /\ A e. _V ) -> ( E. y e. B ps -> th ) ) |
24 |
9 23
|
mpd |
|- ( ( ph /\ A e. _V ) -> th ) |
25 |
8 24
|
sylan2 |
|- ( ( ph /\ A e. V ) -> th ) |