Theorem spc2d

Description: 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	spc2d	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( A. x A. y ps -> ch ) )

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		2nalexn	|- ( -. A. x A. y ps <-> E. x E. y -. ps )
5	4	con1bii	|- ( -. E. x E. y -. ps <-> A. x A. y ps )
6	1	nfn	|- F/ x -. ch
7	2	nfn	|- F/ y -. ch
8	3	notbid	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( -. ps <-> -. ch ) )
9	6 7 8	spc2ed	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( -. ch -> E. x E. y -. ps ) )
10	9	con1d	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( -. E. x E. y -. ps -> ch ) )
11	5 10	biimtrrid	|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( A. x A. y ps -> ch ) )