Theorem ac6s3f

Description: Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018)

	Ref	Expression
Hypotheses	ac6s3f.1	⊢ Ⅎ 𝑦 𝜓
	ac6s3f.2	⊢ 𝐴 ∈ V
	ac6s3f.3	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	ac6s3f	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ac6s3f.1	⊢ Ⅎ 𝑦 𝜓
2		ac6s3f.2	⊢ 𝐴 ∈ V
3		ac6s3f.3	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) )
4		rexv	⊢ ( ∃ 𝑦 ∈ V 𝜑 ↔ ∃ 𝑦 𝜑 )
5	4	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 )
6	5	biimpri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 )
7	1 2 3	ac6sf	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ V 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )
8		exsimpr	⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 𝜓 )
9	6 7 8	3syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 𝜓 )