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

Metamath Proof Explorer

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