Metamath Proof Explorer

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 
|- Fin7 = Fin

Proof

Step Hyp Ref Expression
1 axac3 
 |-  CHOICE
2 dfacfin7 
 |-  ( CHOICE <-> Fin7 = Fin )
3 1 2 mpbi 
 |-  Fin7 = Fin