Theorem ac6sf

Description: Version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008)

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

Proof

Step	Hyp	Ref	Expression
1		ac6sf.1	$$⊢Ⅎy\psi$$
2		ac6sf.2	$$⊢A\in \mathrm{V}$$
3		ac6sf.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
4		cbvrexsvw	$$⊢\exists y\in B\phi \leftrightarrow \exists z\in B\left[z/y\right]\phi$$
5	4	ralbii	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \forall x\in A\exists z\in B\left[z/y\right]\phi$$
6	1 3	sbhypf	$$⊢z=f\left(x\right)\to \left(\left[z/y\right]\phi \leftrightarrow \psi \right)$$
7	2 6	ac6s	$$⊢\forall x\in A\exists z\in B\left[z/y\right]\phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$
8	5 7	sylbi	$$⊢\forall x\in A\exists y\in B\phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$