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	|- ( ph -> G Fn _V )
	gblacfnac2d.2	|- ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
Assertion	gblacfnac2d	|- ( ph -> CHOICE )

Proof

Step	Hyp	Ref	Expression
1		gblacfnac2d.1	|- ( ph -> G Fn _V )
2		gblacfnac2d.2	|- ( ph -> A. z ( z =/= (/) -> ( G ` z ) e. z ) )
3	1 2	gblacfnacd	|- ( ph -> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) )
4		dfac4	|- ( CHOICE <-> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) )
5	3 4	sylibr	|- ( ph -> CHOICE )