Theorem ac5

Description: An Axiom of Choice equivalent: there exists a function f (called a choice function) with domain A that maps each nonempty member of the domain to an element of that member. Axiom AC of BellMachover p. 488. Note that the assertion that f be a function is not necessary; see ac4 . (Contributed by NM, 29-Aug-1999)

	Ref	Expression
Hypothesis	ac5.1	⊢ 𝐴 ∈ V
Assertion	ac5	⊢ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ac5.1	⊢ 𝐴 ∈ V
2		fneq2	⊢ ( 𝑦 = 𝐴 → ( 𝑓 Fn 𝑦 ↔ 𝑓 Fn 𝐴 ) )
3		raleq	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
4	2 3	anbi12d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
5	4	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) ) )
6		dfac4	⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) )
7	6	axaci	⊢ ∃ 𝑓 ( 𝑓 Fn 𝑦 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )
8	1 5 7	vtocl	⊢ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) )