Theorem ac6

Description: Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a larger set B , where ph depends on x (the natural number) and y (to specify a member of B ). A stronger version of this theorem, ac6s , allows B to be a proper class. (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	ac6.1	|- A e. _V
	ac6.2	|- B e. _V
	ac6.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion	ac6	|- ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		ac6.1	|- A e. _V
2		ac6.2	|- B e. _V
3		ac6.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
4		ssrab2	|- { y e. B | ph } C_ B
5	4	rgenw	|- A. x e. A { y e. B | ph } C_ B
6		iunss	|- ( U_ x e. A { y e. B | ph } C_ B <-> A. x e. A { y e. B | ph } C_ B )
7	5 6	mpbir	|- U_ x e. A { y e. B | ph } C_ B
8	2 7	ssexi	|- U_ x e. A { y e. B | ph } e. _V
9		numth3	|- ( U_ x e. A { y e. B | ph } e. _V -> U_ x e. A { y e. B | ph } e. dom card )
10	8 9	ax-mp	|- U_ x e. A { y e. B | ph } e. dom card
11	3	ac6num	|- ( ( A e. _V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
12	1 10 11	mp3an12	|- ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )