Step |
Hyp |
Ref |
Expression |
1 |
|
eusvnf |
|- ( E! y A. x y = A -> F/_ x A ) |
2 |
|
euex |
|- ( E! y A. x y = A -> E. y A. x y = A ) |
3 |
|
eqvisset |
|- ( y = A -> A e. _V ) |
4 |
3
|
sps |
|- ( A. x y = A -> A e. _V ) |
5 |
4
|
exlimiv |
|- ( E. y A. x y = A -> A e. _V ) |
6 |
2 5
|
syl |
|- ( E! y A. x y = A -> A e. _V ) |
7 |
1 6
|
jca |
|- ( E! y A. x y = A -> ( F/_ x A /\ A e. _V ) ) |
8 |
|
isset |
|- ( A e. _V <-> E. y y = A ) |
9 |
|
nfcvd |
|- ( F/_ x A -> F/_ x y ) |
10 |
|
id |
|- ( F/_ x A -> F/_ x A ) |
11 |
9 10
|
nfeqd |
|- ( F/_ x A -> F/ x y = A ) |
12 |
11
|
nf5rd |
|- ( F/_ x A -> ( y = A -> A. x y = A ) ) |
13 |
12
|
eximdv |
|- ( F/_ x A -> ( E. y y = A -> E. y A. x y = A ) ) |
14 |
8 13
|
syl5bi |
|- ( F/_ x A -> ( A e. _V -> E. y A. x y = A ) ) |
15 |
14
|
imp |
|- ( ( F/_ x A /\ A e. _V ) -> E. y A. x y = A ) |
16 |
|
eusv1 |
|- ( E! y A. x y = A <-> E. y A. x y = A ) |
17 |
15 16
|
sylibr |
|- ( ( F/_ x A /\ A e. _V ) -> E! y A. x y = A ) |
18 |
7 17
|
impbii |
|- ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) ) |