Step |
Hyp |
Ref |
Expression |
1 |
|
nfa1 |
|- F/ y A. y A. z E* x ph |
2 |
|
nfe1 |
|- F/ y E. y E. z ( A = <. y , z >. /\ ph ) |
3 |
2
|
nfmov |
|- F/ y E* x E. y E. z ( A = <. y , z >. /\ ph ) |
4 |
|
nfa1 |
|- F/ z A. z E* x ph |
5 |
|
nfe1 |
|- F/ z E. z ( A = <. y , z >. /\ ph ) |
6 |
5
|
nfex |
|- F/ z E. y E. z ( A = <. y , z >. /\ ph ) |
7 |
6
|
nfmov |
|- F/ z E* x E. y E. z ( A = <. y , z >. /\ ph ) |
8 |
|
copsexgw |
|- ( A = <. y , z >. -> ( ph <-> E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
9 |
8
|
mobidv |
|- ( A = <. y , z >. -> ( E* x ph <-> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
10 |
9
|
biimpcd |
|- ( E* x ph -> ( A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
11 |
10
|
sps |
|- ( A. z E* x ph -> ( A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
12 |
4 7 11
|
exlimd |
|- ( A. z E* x ph -> ( E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
13 |
12
|
sps |
|- ( A. y A. z E* x ph -> ( E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
14 |
1 3 13
|
exlimd |
|- ( A. y A. z E* x ph -> ( E. y E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) ) |
15 |
|
simpl |
|- ( ( A = <. y , z >. /\ ph ) -> A = <. y , z >. ) |
16 |
15
|
2eximi |
|- ( E. y E. z ( A = <. y , z >. /\ ph ) -> E. y E. z A = <. y , z >. ) |
17 |
16
|
exlimiv |
|- ( E. x E. y E. z ( A = <. y , z >. /\ ph ) -> E. y E. z A = <. y , z >. ) |
18 |
|
nexmo |
|- ( -. E. x E. y E. z ( A = <. y , z >. /\ ph ) -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) |
19 |
17 18
|
nsyl5 |
|- ( -. E. y E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) |
20 |
14 19
|
pm2.61d1 |
|- ( A. y A. z E* x ph -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) |