# Metamath Proof Explorer

## Theorem ixp0

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 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}=\varnothing \to \underset{{x}\in {A}}{⨉}{B}=\varnothing$

### Proof

Step Hyp Ref Expression
1 nne ${⊢}¬{B}\ne \varnothing ↔{B}=\varnothing$
2 1 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}\ne \varnothing ↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}=\varnothing$
3 rexnal ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{B}\ne \varnothing ↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
4 2 3 bitr3i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}=\varnothing ↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
5 ixpn0 ${⊢}\underset{{x}\in {A}}{⨉}{B}\ne \varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
6 5 necon1bi ${⊢}¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing \to \underset{{x}\in {A}}{⨉}{B}=\varnothing$
7 4 6 sylbi ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}=\varnothing \to \underset{{x}\in {A}}{⨉}{B}=\varnothing$