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

Metamath Proof Explorer

Theorem ac6gf

Description: Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses ac6gf.1 
|- F/ y ps
ac6gf.2 
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6gf 
|- ( ( A e. C /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 ac6gf.1 
 |-  F/ y ps
2 ac6gf.2 
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
3 cbvrexsvw 
 |-  ( E. y e. B ph <-> E. z e. B [ z / y ] ph )
4 3 ralbii 
 |-  ( A. x e. A E. y e. B ph <-> A. x e. A E. z e. B [ z / y ] ph )
5 1 2 sbhypf 
 |-  ( z = ( f ` x ) -> ( [ z / y ] ph <-> ps ) )
6 5 ac6sg 
 |-  ( A e. C -> ( A. x e. A E. z e. B [ z / y ] ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) )
7 6 imp 
 |-  ( ( A e. C /\ A. x e. A E. z e. B [ z / y ] ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
8 4 7 sylan2b 
 |-  ( ( A e. C /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )