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

Metamath Proof Explorer

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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) )