Metamath Proof Explorer

Theorem ac9

Description: An Axiom of Choice equivalent: the infinite Cartesian product of nonempty classes is nonempty. Axiom of Choice (second form) of Enderton p. 55 and its converse. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 ⊢A∈V
ac6c4.2 ⊢B∈V
Assertion ac9 ⊢∀x∈AB≠∅↔⨉x∈AB≠∅

Proof

Step Hyp Ref Expression
1 ac6c4.1 ⊢A∈V
2 ac6c4.2 ⊢B∈V
3 1 2 ac6c4 ⊢∀x∈AB≠∅→∃ffFnA∧∀x∈Af⁡x∈B
4 n0 ⊢⨉x∈AB≠∅↔∃ff∈⨉x∈AB
5 vex ⊢f∈V
6 5 elixp ⊢f∈⨉x∈AB↔fFnA∧∀x∈Af⁡x∈B
7 6 exbii ⊢∃ff∈⨉x∈AB↔∃ffFnA∧∀x∈Af⁡x∈B
8 4 7 bitr2i ⊢∃ffFnA∧∀x∈Af⁡x∈B↔⨉x∈AB≠∅
9 3 8 sylib ⊢∀x∈AB≠∅→⨉x∈AB≠∅
10 ixpn0 ⊢⨉x∈AB≠∅→∀x∈AB≠∅
11 9 10 impbii ⊢∀x∈AB≠∅↔⨉x∈AB≠∅