Theorem ac9s

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. This is a stronger version of the axiom in Enderton, with no existence requirement for the family of classes B ( x ) (achieved via the Collection Principle cp ). (Contributed by NM, 29-Sep-2006)

	Ref	Expression
Hypothesis	ac9.1	|- A e. _V
Assertion	ac9s	|- ( A. x e. A B =/= (/) <-> X_ x e. A B =/= (/) )

Proof

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