Theorem spc2egv

Description: Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995)

	Ref	Expression
Hypothesis	spc2egv.1	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
Assertion	spc2egv	|- ( ( A e. V /\ B e. W ) -> ( ps -> E. x E. y ph ) )

Proof

Step	Hyp	Ref	Expression
1		spc2egv.1	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2		elisset	|- ( A e. V -> E. x x = A )
3		elisset	|- ( B e. W -> E. y y = B )
4	2 3	anim12i	|- ( ( A e. V /\ B e. W ) -> ( E. x x = A /\ E. y y = B ) )
5		exdistrv	|- ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
6	4 5	sylibr	|- ( ( A e. V /\ B e. W ) -> E. x E. y ( x = A /\ y = B ) )
7	1	biimprcd	|- ( ps -> ( ( x = A /\ y = B ) -> ph ) )
8	7	2eximdv	|- ( ps -> ( E. x E. y ( x = A /\ y = B ) -> E. x E. y ph ) )
9	6 8	syl5com	|- ( ( A e. V /\ B e. W ) -> ( ps -> E. x E. y ph ) )