Theorem ac6s3f

Description: Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ac6s3f.1	$$⊢Ⅎy\psi$$
2		ac6s3f.2	$$⊢A\in \mathrm{V}$$
3		ac6s3f.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
4		rexv	$$⊢\exists y\in \mathrm{V}\phi \leftrightarrow \exists y\phi$$
5	4	ralbii	$$⊢\forall x\in A\exists y\in \mathrm{V}\phi \leftrightarrow \forall x\in A\exists y\phi$$
6	5	biimpri	$$⊢\forall x\in A\exists y\phi \to \forall x\in A\exists y\in \mathrm{V}\phi$$
7	1 2 3	ac6sf	$$⊢\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)$$
8		exsimpr	$$⊢\exists f\left(f:A⟶\mathrm{V}\wedge \forall x\in A\psi \right)\to \exists f\forall x\in A\psi$$
9	6 7 8	3syl	$$⊢\forall x\in A\exists y\phi \to \exists f\forall x\in A\psi$$