Metamath Proof Explorer

Theorem lbsex

Description: Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypothesis lbsex.j 
|- J = ( LBasis ` W )
Assertion lbsex 
|- ( W e. LVec -> J =/= (/) )

Proof

Step Hyp Ref Expression
1 lbsex.j 
 |-  J = ( LBasis ` W )
2 axac3 
 |-  CHOICE
3 1 lbsexg 
 |-  ( ( CHOICE /\ W e. LVec ) -> J =/= (/) )
4 2 3 mpan 
 |-  ( W e. LVec -> J =/= (/) )