# 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 e. _V`
ac6c4.2
`|- B e. _V`
Assertion ac9
`|- ( A. x e. A B =/= (/) <-> X_ x e. A B =/= (/) )`

### Proof

Step Hyp Ref Expression
1 ac6c4.1
` |-  A e. _V`
2 ac6c4.2
` |-  B e. _V`
3 1 2 ac6c4
` |-  ( A. x e. A B =/= (/) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )`
4 n0
` |-  ( X_ x e. A B =/= (/) <-> E. f f e. X_ x e. A B )`
5 vex
` |-  f e. _V`
6 5 elixp
` |-  ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )`
7 6 exbii
` |-  ( E. f f e. X_ x e. A B <-> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )`
8 4 7 bitr2i
` |-  ( E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) <-> X_ x e. A B =/= (/) )`
9 3 8 sylib
` |-  ( A. x e. A B =/= (/) -> X_ x e. A B =/= (/) )`
10 ixpn0
` |-  ( X_ x e. A B =/= (/) -> A. x e. A B =/= (/) )`
11 9 10 impbii
` |-  ( A. x e. A B =/= (/) <-> X_ x e. A B =/= (/) )`