Theorem ac6

Description: Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a larger set B , where ph depends on x (the natural number) and y (to specify a member of B ). A stronger version of this theorem, ac6s , allows B to be a proper class. Unlike ac6sg , which allows B to be a proper class and so uses the Collection principle bnd2 , this needs neither ax-reg nor ax-inf2 . (Contributed by NM, 18-Oct-1999) (Revised by Mario Carneiro, 27-Aug-2015) Replace hypotheses with antecedents. (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypothesis	ac6.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ac6	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ac6.1	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
2		ssrab2	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵
3	2	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵
4		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 )
5	3 4	mpbir	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵
6		ssexg	⊢ ( ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⊆ 𝐵 ∧ 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V )
7	5 6	mpan	⊢ ( 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V )
8		numth3	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ V → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card )
9	7 8	syl	⊢ ( 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card )
10	1	ac6num	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∈ dom card ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
11	9 10	syl3an2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )