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, 1Oct2006) (Proof shortened by Mario Carneiro, 22Jun2016)
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 = (/) ) 