Theorem ac6s2

Description: Generalization of the Axiom of Choice to classes. Slightly strengthened version of ac6s3 . (Contributed by NM, 29-Sep-2006)

	Ref	Expression
Hypotheses	ac6s.1	⊢ 𝐴 ∈ V
	ac6s.2	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ac6s2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ac6s.1	⊢ 𝐴 ∈ V
2		ac6s.2	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
3		rexv	⊢ ( ∃ 𝑦 ∈ V 𝜑 ↔ ∃ 𝑦 𝜑 )
4	3	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 )
5	1 2	ac6s	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
6		ffn	⊢ ( 𝑓 : 𝐴 ⟶ V → 𝑓 Fn 𝐴 )
7	6	anim1i	⊢ ( ( 𝑓 : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
8	7	eximi	⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
9	5 8	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
10	4 9	sylbir	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )