Theorem ac6s2

Description: Generalization of the Axiom of Choice to classes. Slightly strengthened version of ac6s3 . (Contributed by NM, 29-Sep-2006)

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

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		rexv	$$⊢\exists y\in \mathrm{V}\phi \leftrightarrow \exists y\phi$$
4	3	ralbii	$$⊢\forall x\in A\exists y\in \mathrm{V}\phi \leftrightarrow \forall x\in A\exists y\phi$$
5	1 2	ac6s	$$⊢\forall x\in A\exists y\in \mathrm{V}\phi \to \exists f\left(f:A⟶\mathrm{V}\wedge \forall x\in A\psi \right)$$
6		ffn	$$⊢f:A⟶\mathrm{V}\to fFnA$$
7	6	anim1i	$$⊢\left(f:A⟶\mathrm{V}\wedge \forall x\in A\psi \right)\to \left(fFnA\wedge \forall x\in A\psi \right)$$
8	7	eximi	$$⊢\exists f\left(f:A⟶\mathrm{V}\wedge \forall x\in A\psi \right)\to \exists f\left(fFnA\wedge \forall x\in A\psi \right)$$
9	5 8	syl	$$⊢\forall x\in A\exists y\in \mathrm{V}\phi \to \exists f\left(fFnA\wedge \forall x\in A\psi \right)$$
10	4 9	sylbir	$$⊢\forall x\in A\exists y\phi \to \exists f\left(fFnA\wedge \forall x\in A\psi \right)$$