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

Metamath Proof Explorer

Theorem dfac10

Description: Axiom of Choice equivalent: the cardinality function measures every set. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion dfac10 ⊢ CHOICE ↔ dom ⁡ card = V

Proof

Step Hyp Ref Expression
1 ween ⊢ x ∈ dom ⁡ card ↔ ∃ y y We x
2 1 albii ⊢ ∀ x x ∈ dom ⁡ card ↔ ∀ x ∃ y y We x
3 eqv ⊢ dom ⁡ card = V ↔ ∀ x x ∈ dom ⁡ card
4 dfac8 ⊢ CHOICE ↔ ∀ x ∃ y y We x
5 2 3 4 3bitr4ri ⊢ CHOICE ↔ dom ⁡ card = V