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	⊢ ( 𝜑 → 𝐺 Fn V )
	gblacfnac2d.2	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
Assertion	gblacfnac2d	⊢ ( 𝜑 → CHOICE )

Proof

Step	Hyp	Ref	Expression
1		gblacfnac2d.1	⊢ ( 𝜑 → 𝐺 Fn V )
2		gblacfnac2d.2	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
3	1 2	gblacfnacd	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
4		dfac4	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ( 𝑓 Fn 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
5	3 4	sylibr	⊢ ( 𝜑 → CHOICE )