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

Metamath Proof Explorer

Theorem ac4c

Description: Equivalent of Axiom of Choice (class version). (Contributed by NM, 10-Feb-1997)

Ref Expression
Hypothesis ac4c.1 ⊢ A ∈ V
Assertion ac4c ⊢ ∃ f ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x

Proof

Step Hyp Ref Expression
1 ac4c.1 ⊢ A ∈ V
2 raleq ⊢ y = A → ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x ↔ ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x
3 2 exbidv ⊢ y = A → ∃ f ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x ↔ ∃ f ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x
4 ac4 ⊢ ∃ f ∀ x ∈ y x ≠ ∅ → f ⁡ x ∈ x
5 1 3 4 vtocl ⊢ ∃ f ∀ x ∈ A x ≠ ∅ → f ⁡ x ∈ x