Theorem gblacfnac2d

Description: If G is a global choice function, then the Axiom of Choice holds. This is gblacfnacd expressed using CHOICE . (Contributed by BTernaryTau, 25-Sep-2026)

	Ref	Expression
Hypotheses	gblacfnac2d.1	$$⊢\phi \to GFn\mathrm{V}$$
	gblacfnac2d.2	$$⊢\phi \to \forall z\left(z\ne \varnothing \to G\left(z\right)\in z\right)$$
Assertion	gblacfnac2d	$$⊢\phi \to \mathrm{CHOICE}$$

Proof

Step	Hyp	Ref	Expression
1		gblacfnac2d.1	$$⊢\phi \to GFn\mathrm{V}$$
2		gblacfnac2d.2	$$⊢\phi \to \forall z\left(z\ne \varnothing \to G\left(z\right)\in z\right)$$
3	1 2	gblacfnacd	$$⊢\phi \to \forall x\exists f\left(fFnx\wedge \forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)\right)$$
4		dfac4	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists f\left(fFnx\wedge \forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)\right)$$
5	3 4	sylibr	$$⊢\phi \to \mathrm{CHOICE}$$