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. Unlike ac6sg , which allows B to be a proper class and so uses the Collection principle bnd2 , this needs neither ax-reg nor ax-inf2 . (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015) Replace hypotheses with antecedents. (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypothesis	ac6.1	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion	ac6	|- ( ( A e. V /\ B e. W /\ 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	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
2		ssrab2	|- { y e. B | ph } C_ B
3	2	rgenw	|- A. x e. A { y e. B | ph } C_ B
4		iunss	|- ( U_ x e. A { y e. B | ph } C_ B <-> A. x e. A { y e. B | ph } C_ B )
5	3 4	mpbir	|- U_ x e. A { y e. B | ph } C_ B
6		ssexg	|- ( ( U_ x e. A { y e. B | ph } C_ B /\ B e. W ) -> U_ x e. A { y e. B | ph } e. _V )
7	5 6	mpan	|- ( B e. W -> U_ x e. A { y e. B | ph } e. _V )
8		numth3	|- ( U_ x e. A { y e. B | ph } e. _V -> U_ x e. A { y e. B | ph } e. dom card )
9	7 8	syl	|- ( B e. W -> U_ x e. A { y e. B | ph } e. dom card )
10	1	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 ) )
11	9 10	syl3an2	|- ( ( A e. V /\ B e. W /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )