Theorem ac6sf

Description: Version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008)

	Ref	Expression
Hypotheses	ac6sf.1	|- F/ y ps
	ac6sf.2	|- A e. _V
	ac6sf.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion	ac6sf	|- ( 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		ac6sf.1	|- F/ y ps
2		ac6sf.2	|- A e. _V
3		ac6sf.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
4		cbvrexsvw	|- ( E. y e. B ph <-> E. z e. B [ z / y ] ph )
5	4	ralbii	|- ( A. x e. A E. y e. B ph <-> A. x e. A E. z e. B [ z / y ] ph )
6	1 3	sbhypf	|- ( z = ( f ` x ) -> ( [ z / y ] ph <-> ps ) )
7	2 6	ac6s	|- ( A. x e. A E. z e. B [ z / y ] ph -> E. f ( f : A --> B /\ A. x e. A ps ) )
8	5 7	sylbi	|- ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )