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\in \mathrm{V}$$
	ac6.2	$$⊢B\in \mathrm{V}$$
	ac6.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6	$$⊢\forall x\in A\exists y\in B\phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ac6.1	$$⊢A\in \mathrm{V}$$
2		ac6.2	$$⊢B\in \mathrm{V}$$
3		ac6.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
4		ssrab2	$$⊢\left\{y\in B|\phi \right\}\subseteq B$$
5	4	rgenw	$$⊢\forall x\in A\left\{y\in B|\phi \right\}\subseteq B$$
6		iunss	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\subseteq B\leftrightarrow \forall x\in A\left\{y\in B|\phi \right\}\subseteq B$$
7	5 6	mpbir	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\subseteq B$$
8	2 7	ssexi	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{V}$$
9		numth3	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{V}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}$$
10	8 9	ax-mp	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}$$
11	3	ac6num	$$⊢\left(A\in \mathrm{V}\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$
12	1 10 11	mp3an12	$$⊢\forall x\in A\exists y\in B\phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$