This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ac5

Description: An Axiom of Choice equivalent: there exists a function f (called a choice function) with domain A that maps each nonempty member of the domain to an element of that member. Axiom AC of BellMachover p. 488. Note that the assertion that f be a function is not necessary; see ac4 . (Contributed by NM, 29-Aug-1999)

Ref Expression
Hypothesis ac5.1 
|- A e. _V
Assertion ac5 
|- E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) )

Proof

Step Hyp Ref Expression
1 ac5.1 
 |-  A e. _V
2 fneq2 
 |-  ( y = A -> ( f Fn y <-> f Fn A ) )
3 raleq 
 |-  ( y = A -> ( A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )
4 2 3 anbi12d 
 |-  ( y = A -> ( ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
5 4 exbidv 
 |-  ( y = A -> ( E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) <-> E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
6 dfac4 
 |-  ( CHOICE <-> A. y E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) )
7 6 axaci 
 |-  E. f ( f Fn y /\ A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
8 1 5 7 vtocl 
 |-  E. f ( f Fn A /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) )