This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ac6s5

Description: Generalization of the Axiom of Choice to proper classes. B is a collection B ( x ) of nonempty, possible proper classes. Remark after Theorem 10.46 of TakeutiZaring p. 98. (Contributed by NM, 27-Mar-2006)

		Ref	Expression
	Hypothesis	ac6s4.1	⊢ 𝐴 ∈ V
	Assertion	ac6s5	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ac6s4.1	⊢ 𝐴 ∈ V
2	1	ac6s4	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
3		exsimpr	⊢ ( ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
4	2 3	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )