Theorem ac5b

Description: Equivalent of Axiom of Choice. (Contributed by NM, 31-Aug-1999)

	Ref	Expression
Hypothesis	ac5b.1	$$⊢A\in \mathrm{V}$$
Assertion	ac5b	$$⊢\forall x\in Ax\ne \varnothing \to \exists f\left(f:A⟶\bigcup A\wedge \forall x\in Af\left(x\right)\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		ac5b.1	$$⊢A\in \mathrm{V}$$
2	1	uniex	$$⊢\bigcup A\in \mathrm{V}$$
3		numth3	$$⊢\bigcup A\in \mathrm{V}\to \bigcup A\in \mathrm{dom}\mathrm{card}$$
4	2 3	mp1i	$$⊢\forall x\in Ax\ne \varnothing \to \bigcup A\in \mathrm{dom}\mathrm{card}$$
5		neirr	$$⊢\neg \varnothing \ne \varnothing$$
6		neeq1	$$⊢x=\varnothing \to \left(x\ne \varnothing \leftrightarrow \varnothing \ne \varnothing \right)$$
7	6	rspccv	$$⊢\forall x\in Ax\ne \varnothing \to \left(\varnothing \in A\to \varnothing \ne \varnothing \right)$$
8	5 7	mtoi	$$⊢\forall x\in Ax\ne \varnothing \to \neg \varnothing \in A$$
9		ac5num	$$⊢\left(\bigcup A\in \mathrm{dom}\mathrm{card}\wedge \neg \varnothing \in A\right)\to \exists f\left(f:A⟶\bigcup A\wedge \forall x\in Af\left(x\right)\in x\right)$$
10	4 8 9	syl2anc	$$⊢\forall x\in Ax\ne \varnothing \to \exists f\left(f:A⟶\bigcup A\wedge \forall x\in Af\left(x\right)\in x\right)$$