Step |
Hyp |
Ref |
Expression |
1 |
|
ne0i |
|- ( X e. { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } -> { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } =/= (/) ) |
2 |
|
abn0 |
|- ( { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } =/= (/) <-> E. x ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) ) |
3 |
|
simpl |
|- ( ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) -> A e. _V ) |
4 |
3
|
exlimiv |
|- ( E. x ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) -> A e. _V ) |
5 |
2 4
|
sylbi |
|- ( { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } =/= (/) -> A e. _V ) |
6 |
1 5
|
syl |
|- ( X e. { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } -> A e. _V ) |
7 |
|
df-acn |
|- AC_ A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } |
8 |
6 7
|
eleq2s |
|- ( X e. AC_ A -> A e. _V ) |