Theorem ac6sf2

Description: Alternate version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008) (Revised by Thierry Arnoux, 17-May-2020)

	Ref	Expression
Hypotheses	ac6sf2.y	$$⊢\underset{\_}{Ⅎ}yB$$
	ac6sf2.1	$$⊢Ⅎy\psi$$
	ac6sf2.2	$$⊢A\in \mathrm{V}$$
	ac6sf2.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6sf2	$$⊢\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		ac6sf2.y	$$⊢\underset{\_}{Ⅎ}yB$$
2		ac6sf2.1	$$⊢Ⅎy\psi$$
3		ac6sf2.2	$$⊢A\in \mathrm{V}$$
4		ac6sf2.3	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}zB$$
6		nfv	$$⊢Ⅎz\phi$$
7		nfs1v	$$⊢Ⅎy\left[z/y\right]\phi$$
8		sbequ12	$$⊢y=z\to \left(\phi \leftrightarrow \left[z/y\right]\phi \right)$$
9	1 5 6 7 8	cbvrexfw	$$⊢\exists y\in B\phi \leftrightarrow \exists z\in B\left[z/y\right]\phi$$
10	9	ralbii	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \forall x\in A\exists z\in B\left[z/y\right]\phi$$
11	2 4	sbhypf	$$⊢z=f\left(x\right)\to \left(\left[z/y\right]\phi \leftrightarrow \psi \right)$$
12	3 11	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)$$
13	10 12	sylbi	$$⊢\forall x\in A\exists y\in B\phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$