# Metamath Proof Explorer

## Theorem ac9

Description: An Axiom of Choice equivalent: the infinite Cartesian product of nonempty classes is nonempty. Axiom of Choice (second form) of Enderton p. 55 and its converse. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 ${⊢}{A}\in \mathrm{V}$
ac6c4.2 ${⊢}{B}\in \mathrm{V}$
Assertion ac9 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing ↔\underset{{x}\in {A}}{⨉}{B}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 ac6c4.1 ${⊢}{A}\in \mathrm{V}$
2 ac6c4.2 ${⊢}{B}\in \mathrm{V}$
3 1 2 ac6c4 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing \to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
4 n0 ${⊢}\underset{{x}\in {A}}{⨉}{B}\ne \varnothing ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \underset{{x}\in {A}}{⨉}{B}$
5 vex ${⊢}{f}\in \mathrm{V}$
6 5 elixp ${⊢}{f}\in \underset{{x}\in {A}}{⨉}{B}↔\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
7 6 exbii ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \underset{{x}\in {A}}{⨉}{B}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
8 4 7 bitr2i ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)↔\underset{{x}\in {A}}{⨉}{B}\ne \varnothing$
9 3 8 sylib ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing \to \underset{{x}\in {A}}{⨉}{B}\ne \varnothing$
10 ixpn0 ${⊢}\underset{{x}\in {A}}{⨉}{B}\ne \varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing$
11 9 10 impbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\ne \varnothing ↔\underset{{x}\in {A}}{⨉}{B}\ne \varnothing$