Metamath Proof Explorer


Theorem dfac7

Description: Equivalence of the Axiom of Choice (first form) of Enderton p. 49 and our Axiom of Choice (in the form of ac2 ). The proof does not depend on AC but does depend on the Axiom of Regularity. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfac7 ( CHOICE ↔ ∀ 𝑥𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) )

Proof

Step Hyp Ref Expression
1 dfac2 ( CHOICE ↔ ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
2 aceq2 ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
3 2 albii ( ∀ 𝑥𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
4 1 3 bitr4i ( CHOICE ↔ ∀ 𝑥𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) )