Step |
Hyp |
Ref |
Expression |
1 |
|
nfra1 |
|- F/ y A. y e. B ( ph -> x = C ) |
2 |
1
|
nfmov |
|- F/ y E* x A. y e. B ( ph -> x = C ) |
3 |
|
rsp |
|- ( A. y e. B ( ph -> x = C ) -> ( y e. B -> ( ph -> x = C ) ) ) |
4 |
3
|
com3l |
|- ( y e. B -> ( ph -> ( A. y e. B ( ph -> x = C ) -> x = C ) ) ) |
5 |
4
|
alrimdv |
|- ( y e. B -> ( ph -> A. x ( A. y e. B ( ph -> x = C ) -> x = C ) ) ) |
6 |
|
mo2icl |
|- ( A. x ( A. y e. B ( ph -> x = C ) -> x = C ) -> E* x A. y e. B ( ph -> x = C ) ) |
7 |
5 6
|
syl6 |
|- ( y e. B -> ( ph -> E* x A. y e. B ( ph -> x = C ) ) ) |
8 |
2 7
|
rexlimi |
|- ( E. y e. B ph -> E* x A. y e. B ( ph -> x = C ) ) |
9 |
|
mormo |
|- ( E* x A. y e. B ( ph -> x = C ) -> E* x e. A A. y e. B ( ph -> x = C ) ) |
10 |
|
reu5 |
|- ( E! x e. A A. y e. B ( ph -> x = C ) <-> ( E. x e. A A. y e. B ( ph -> x = C ) /\ E* x e. A A. y e. B ( ph -> x = C ) ) ) |
11 |
10
|
rbaib |
|- ( E* x e. A A. y e. B ( ph -> x = C ) -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) ) |
12 |
8 9 11
|
3syl |
|- ( E. y e. B ph -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) ) |