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	$$⊢{\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		axac3	$$⊢\mathrm{CHOICE}$$
2		dfacfin7	$$⊢\mathrm{CHOICE}\leftrightarrow {\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}$$
3	1 2	mpbi	$$⊢{\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}$$