Metamath Proof Explorer

Theorem ac6sg

Description: ac6s with sethood as antecedent. (Contributed by FL, 3-Aug-2009)

Ref Expression
Hypothesis ac6sg.1 
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6sg 
|- ( A e. V -> ( 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 ac6sg.1 
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
2 raleq 
 |-  ( z = A -> ( A. x e. z E. y e. B ph <-> A. x e. A E. y e. B ph ) )
3 feq2 
 |-  ( z = A -> ( f : z --> B <-> f : A --> B ) )
4 raleq 
 |-  ( z = A -> ( A. x e. z ps <-> A. x e. A ps ) )
5 3 4 anbi12d 
 |-  ( z = A -> ( ( f : z --> B /\ A. x e. z ps ) <-> ( f : A --> B /\ A. x e. A ps ) ) )
6 5 exbidv 
 |-  ( z = A -> ( E. f ( f : z --> B /\ A. x e. z ps ) <-> E. f ( f : A --> B /\ A. x e. A ps ) ) )
7 2 6 imbi12d 
 |-  ( z = A -> ( ( A. x e. z E. y e. B ph -> E. f ( f : z --> B /\ A. x e. z ps ) ) <-> ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) ) )
8 vex 
 |-  z e. _V
9 8 1 ac6s 
 |-  ( A. x e. z E. y e. B ph -> E. f ( f : z --> B /\ A. x e. z ps ) )
10 7 9 vtoclg 
 |-  ( A e. V -> ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) )