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 e. dom card <-> E. y y We x )
2 1 albii 
 |-  ( A. x x e. dom card <-> A. x E. y y We x )
3 eqv 
 |-  ( dom card = _V <-> A. x x e. dom card )
4 dfac8 
 |-  ( CHOICE <-> A. x E. y y We x )
5 2 3 4 3bitr4ri 
 |-  ( CHOICE <-> dom card = _V )