Theorem ac6s6f

Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ac6s6f.1	$$⊢A\in \mathrm{V}$$
2		ac6s6f.2	$$⊢Ⅎy\psi$$
3		ac6s6f.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
4		ac6s6f.4	$$⊢\underset{\_}{Ⅎ}xA$$
5	1	isseti	$$⊢\exists zz=A$$
6		vex	$$⊢z\in \mathrm{V}$$
7	2 6 3	ac6s6	$$⊢\exists f\forall x\in z\left(\exists y\phi \to \psi \right)$$
8	5 7	exan	$$⊢\exists z\left(z=A\wedge \exists f\forall x\in z\left(\exists y\phi \to \psi \right)\right)$$
9		exdistr	$$⊢\exists z\exists f\left(z=A\wedge \forall x\in z\left(\exists y\phi \to \psi \right)\right)\leftrightarrow \exists z\left(z=A\wedge \exists f\forall x\in z\left(\exists y\phi \to \psi \right)\right)$$
10	8 9	mpbir	$$⊢\exists z\exists f\left(z=A\wedge \forall x\in z\left(\exists y\phi \to \psi \right)\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
12	11 4	raleqf	$$⊢z=A\to \left(\forall x\in z\left(\exists y\phi \to \psi \right)\leftrightarrow \forall x\in A\left(\exists y\phi \to \psi \right)\right)$$
13	12	biimpa	$$⊢\left(z=A\wedge \forall x\in z\left(\exists y\phi \to \psi \right)\right)\to \forall x\in A\left(\exists y\phi \to \psi \right)$$
14	13	2eximi	$$⊢\exists z\exists f\left(z=A\wedge \forall x\in z\left(\exists y\phi \to \psi \right)\right)\to \exists z\exists f\forall x\in A\left(\exists y\phi \to \psi \right)$$
15		ax5e	$$⊢\exists z\exists f\forall x\in A\left(\exists y\phi \to \psi \right)\to \exists f\forall x\in A\left(\exists y\phi \to \psi \right)$$
16	10 14 15	mp2b	$$⊢\exists f\forall x\in A\left(\exists y\phi \to \psi \right)$$