Metamath Proof Explorer

Theorem acnrcl

Description: Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnrcl ⊢X∈AC_A→A∈V

Proof

Step Hyp Ref Expression
1 ne0i ⊢X∈x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y→x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y≠∅
2 abn0 ⊢x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y≠∅↔∃xA∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
3 simpl ⊢A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y→A∈V
4 3 exlimiv ⊢∃xA∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y→A∈V
5 2 4 sylbi ⊢x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y≠∅→A∈V
6 1 5 syl ⊢X∈x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y→A∈V
7 df-acn ⊢AC_A=x|A∈V∧∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
8 6 7 eleq2s ⊢X∈AC_A→A∈V