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