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