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

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 ) )