Theorem ac6sf2

Description: Alternate version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008) (Revised by Thierry Arnoux, 17-May-2020)

	Ref	Expression
Hypotheses	ac6sf2.y	|- F/_ y B
	ac6sf2.1	|- F/ y ps
	ac6sf2.2	|- A e. _V
	ac6sf2.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion	ac6sf2	|- ( 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		ac6sf2.y	|- F/_ y B
2		ac6sf2.1	|- F/ y ps
3		ac6sf2.2	|- A e. _V
4		ac6sf2.3	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
5		nfcv	|- F/_ z B
6		nfv	|- F/ z ph
7		nfs1v	|- F/ y [ z / y ] ph
8		sbequ12	|- ( y = z -> ( ph <-> [ z / y ] ph ) )
9	1 5 6 7 8	cbvrexfw	|- ( E. y e. B ph <-> E. z e. B [ z / y ] ph )
10	9	ralbii	|- ( A. x e. A E. y e. B ph <-> A. x e. A E. z e. B [ z / y ] ph )
11	2 4	sbhypf	|- ( z = ( f ` x ) -> ( [ z / y ] ph <-> ps ) )
12	3 11	ac6s	|- ( A. x e. A E. z e. B [ z / y ] ph -> E. f ( f : A --> B /\ A. x e. A ps ) )
13	10 12	sylbi	|- ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) )