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

Metamath Proof Explorer

Theorem spc2ed

Description: Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 spc2ed.x 
 |-  F/ x ch
2 spc2ed.y 
 |-  F/ y ch
3 spc2ed.1 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
4 elisset 
 |-  ( A e. V -> E. x x = A )
5 elisset 
 |-  ( B e. W -> E. y y = B )
6 4 5 anim12i 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x x = A /\ E. y y = B ) )
7 exdistrv 
 |-  ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
8 6 7 sylibr 
 |-  ( ( A e. V /\ B e. W ) -> E. x E. y ( x = A /\ y = B ) )
9 nfv 
 |-  F/ x ph
10 9 1 nfan 
 |-  F/ x ( ph /\ ch )
11 nfv 
 |-  F/ y ph
12 11 2 nfan 
 |-  F/ y ( ph /\ ch )
13 anass 
 |-  ( ( ( ch /\ ph ) /\ ( x = A /\ y = B ) ) <-> ( ch /\ ( ph /\ ( x = A /\ y = B ) ) ) )
14 ancom 
 |-  ( ( ch /\ ph ) <-> ( ph /\ ch ) )
15 14 anbi1i 
 |-  ( ( ( ch /\ ph ) /\ ( x = A /\ y = B ) ) <-> ( ( ph /\ ch ) /\ ( x = A /\ y = B ) ) )
16 13 15 bitr3i 
 |-  ( ( ch /\ ( ph /\ ( x = A /\ y = B ) ) ) <-> ( ( ph /\ ch ) /\ ( x = A /\ y = B ) ) )
17 3 biimparc 
 |-  ( ( ch /\ ( ph /\ ( x = A /\ y = B ) ) ) -> ps )
18 16 17 sylbir 
 |-  ( ( ( ph /\ ch ) /\ ( x = A /\ y = B ) ) -> ps )
19 18 ex 
 |-  ( ( ph /\ ch ) -> ( ( x = A /\ y = B ) -> ps ) )
20 12 19 eximd 
 |-  ( ( ph /\ ch ) -> ( E. y ( x = A /\ y = B ) -> E. y ps ) )
21 10 20 eximd 
 |-  ( ( ph /\ ch ) -> ( E. x E. y ( x = A /\ y = B ) -> E. x E. y ps ) )
22 21 impancom 
 |-  ( ( ph /\ E. x E. y ( x = A /\ y = B ) ) -> ( ch -> E. x E. y ps ) )
23 8 22 sylan2 
 |-  ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( ch -> E. x E. y ps ) )