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	⊢ ( 𝑥 ∈ dom card ↔ ∃ 𝑦 𝑦 We 𝑥 )
2	1	albii	⊢ ( ∀ 𝑥 𝑥 ∈ dom card ↔ ∀ 𝑥 ∃ 𝑦 𝑦 We 𝑥 )
3		eqv	⊢ ( dom card = V ↔ ∀ 𝑥 𝑥 ∈ dom card )
4		dfac8	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 𝑦 We 𝑥 )
5	2 3 4	3bitr4ri	⊢ ( CHOICE ↔ dom card = V )