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

Metamath Proof Explorer

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