Metamath Proof Explorer


Theorem ac6s3

Description: Generalization of the Axiom of Choice to classes. Theorem 10.46 of TakeutiZaring p. 97. (Contributed by NM, 3-Nov-2004)

Ref Expression
Hypotheses ac6s.1
|- A e. _V
ac6s.2
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6s3
|- ( A. x e. A E. y ph -> E. f A. x e. A ps )

Proof

Step Hyp Ref Expression
1 ac6s.1
 |-  A e. _V
2 ac6s.2
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
3 1 2 ac6s2
 |-  ( A. x e. A E. y ph -> E. f ( f Fn A /\ A. x e. A ps ) )
4 exsimpr
 |-  ( E. f ( f Fn A /\ A. x e. A ps ) -> E. f A. x e. A ps )
5 3 4 syl
 |-  ( A. x e. A E. y ph -> E. f A. x e. A ps )