Metamath Proof Explorer


Theorem dfac1

Description: Equivalence of two versions of the Axiom of Choice ax-ac . The proof uses the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfac1 CHOICE x y z w z w w x x z x z w w x z x x y z = x

Proof

Step Hyp Ref Expression
1 dfac7 CHOICE x y z x w z ∃! v z u y z u v u
2 aceq1 y z x w z ∃! v z u y z u v u y z w z w w x x z x z w w x z x x y z = x
3 2 albii x y z x w z ∃! v z u y z u v u x y z w z w w x x z x z w w x z x x y z = x
4 1 3 bitri CHOICE x y z w z w w x x z x z w w x z x x y z = x