Theorem ac6gf

Description: Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	ac6gf.1	$$⊢Ⅎy\psi$$
	ac6gf.2	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6gf	$$⊢\left(A\in C\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ac6gf.1	$$⊢Ⅎy\psi$$
2		ac6gf.2	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
3		cbvrexsvw	$$⊢\exists y\in B\phi \leftrightarrow \exists z\in B\left[z/y\right]\phi$$
4	3	ralbii	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \forall x\in A\exists z\in B\left[z/y\right]\phi$$
5	1 2	sbhypf	$$⊢z=f\left(x\right)\to \left(\left[z/y\right]\phi \leftrightarrow \psi \right)$$
6	5	ac6sg	$$⊢A\in C\to \left(\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)\right)$$
7	6	imp	$$⊢\left(A\in C\wedge \forall x\in A\exists z\in B\left[z/y\right]\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$
8	4 7	sylan2b	$$⊢\left(A\in C\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$