Metamath Proof Explorer

Theorem ac7

Description: An Axiom of Choice equivalent similar to the Axiom of Choice (first form) of Enderton p. 49. (Contributed by NM, 29-Apr-2004)

Ref Expression
Assertion ac7 
|- E. f ( f C_ x /\ f Fn dom x )

Proof

Step Hyp Ref Expression
1 df-ac 
 |-  ( CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
2 1 axaci 
 |-  E. f ( f C_ x /\ f Fn dom x )