Theorem ac7

Description: An Axiom of Choice equivalent similar to the Axiom of Choice (first form) of Enderton p. 49. (Contributed by NM, 29-Apr-2004)

	Ref	Expression
Assertion	ac7	$$⊢\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ac	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$
2	1	axaci	$$⊢\exists f\left(f\subseteq x\wedge fFn\mathrm{dom}x\right)$$