Metamath Proof Explorer


Theorem ac6s2

Description: Generalization of the Axiom of Choice to classes. Slightly strengthened version of ac6s3 . (Contributed by NM, 29-Sep-2006)

Ref Expression
Hypotheses ac6s.1
|- A e. _V
ac6s.2
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6s2
|- ( A. x e. A E. y ph -> E. f ( f Fn A /\ 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 rexv
 |-  ( E. y e. _V ph <-> E. y ph )
4 3 ralbii
 |-  ( A. x e. A E. y e. _V ph <-> A. x e. A E. y ph )
5 1 2 ac6s
 |-  ( A. x e. A E. y e. _V ph -> E. f ( f : A --> _V /\ A. x e. A ps ) )
6 ffn
 |-  ( f : A --> _V -> f Fn A )
7 6 anim1i
 |-  ( ( f : A --> _V /\ A. x e. A ps ) -> ( f Fn A /\ A. x e. A ps ) )
8 7 eximi
 |-  ( E. f ( f : A --> _V /\ A. x e. A ps ) -> E. f ( f Fn A /\ A. x e. A ps ) )
9 5 8 syl
 |-  ( A. x e. A E. y e. _V ph -> E. f ( f Fn A /\ A. x e. A ps ) )
10 4 9 sylbir
 |-  ( A. x e. A E. y ph -> E. f ( f Fn A /\ A. x e. A ps ) )