Theorem dfac8c

Description: If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	dfac8c	$$⊢A\in B\to \left(\exists rr\mathrm{We}\bigcup A\to \exists f\forall z\in A\left(z\ne \varnothing \to f\left(z\right)\in z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(x\in \left(A\setminus \left\{\varnothing \right\}\right)⟼\left(\iota y\in x|\forall w\in x\neg wry\right)\right)=\left(x\in \left(A\setminus \left\{\varnothing \right\}\right)⟼\left(\iota y\in x|\forall w\in x\neg wry\right)\right)$$
2	1	dfac8clem	$$⊢A\in B\to \left(\exists rr\mathrm{We}\bigcup A\to \exists f\forall z\in A\left(z\ne \varnothing \to f\left(z\right)\in z\right)\right)$$