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