Theorem fin71ac

Description: Once we allow AC, the "strongest" definition of finite set becomes equivalent to the "weakest" and the entire hierarchy collapses. (Contributed by Stefan O'Rear, 29-Oct-2014)

	Ref	Expression
Assertion	fin71ac	⊢ FinVII = Fin

Proof

Step	Hyp	Ref	Expression
1		axac3	⊢ CHOICE
2		dfacfin7	⊢ ( CHOICE ↔ FinVII = Fin )
3	1 2	mpbi	⊢ FinVII = Fin