Description: Kuratowski's K0 axiom implies K0'. Neighborhood version. Also a proof the dual KA axiom implies KA' when considering the convergents. (Contributed by RP, 28-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | neik0imk0p | |- ( A. x e. B B e. ( N ` x ) -> A. x e. B ( N ` x ) =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ne0i | |- ( B e. ( N ` x ) -> ( N ` x ) =/= (/) ) |
|
| 2 | 1 | ralimi | |- ( A. x e. B B e. ( N ` x ) -> A. x e. B ( N ` x ) =/= (/) ) |