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