This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 =/= (/) )