Description: The infinite Cartesian product of a family B ( x ) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 . (Contributed by NM, 1-Oct-2006) (Proof shortened by Mario Carneiro, 22-Jun-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ixp0 | |- ( E. x e. A B = (/) -> X_ x e. A B = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nne | |- ( -. B =/= (/) <-> B = (/) ) |
|
| 2 | 1 | rexbii | |- ( E. x e. A -. B =/= (/) <-> E. x e. A B = (/) ) |
| 3 | rexnal | |- ( E. x e. A -. B =/= (/) <-> -. A. x e. A B =/= (/) ) |
|
| 4 | 2 3 | bitr3i | |- ( E. x e. A B = (/) <-> -. A. x e. A B =/= (/) ) |
| 5 | ixpn0 | |- ( X_ x e. A B =/= (/) -> A. x e. A B =/= (/) ) |
|
| 6 | 5 | necon1bi | |- ( -. A. x e. A B =/= (/) -> X_ x e. A B = (/) ) |
| 7 | 4 6 | sylbi | |- ( E. x e. A B = (/) -> X_ x e. A B = (/) ) |