Theorem ac6s3

Description: Generalization of the Axiom of Choice to classes. Theorem 10.46 of TakeutiZaring p. 97. (Contributed by NM, 3-Nov-2004)

	Ref	Expression
Hypotheses	ac6s.1	$$⊢A\in \mathrm{V}$$
	ac6s.2	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6s3	$$⊢\forall x\in A\exists y\phi \to \exists f\forall x\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		ac6s.1	$$⊢A\in \mathrm{V}$$
2		ac6s.2	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
3	1 2	ac6s2	$$⊢\forall x\in A\exists y\phi \to \exists f\left(fFnA\wedge \forall x\in A\psi \right)$$
4		exsimpr	$$⊢\exists f\left(fFnA\wedge \forall x\in A\psi \right)\to \exists f\forall x\in A\psi$$
5	3 4	syl	$$⊢\forall x\in A\exists y\phi \to \exists f\forall x\in A\psi$$