Theorem rspc2gv

Description: Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		rspc2gv.1	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2		df-ral	|- ( A. x e. V A. y e. W ph <-> A. x ( x e. V -> A. y e. W ph ) )
3		df-ral	|- ( A. y e. W ph <-> A. y ( y e. W -> ph ) )
4	3	imbi2i	|- ( ( x e. V -> A. y e. W ph ) <-> ( x e. V -> A. y ( y e. W -> ph ) ) )
5	4	albii	|- ( A. x ( x e. V -> A. y e. W ph ) <-> A. x ( x e. V -> A. y ( y e. W -> ph ) ) )
6		19.21v	|- ( A. y ( x e. V -> ( y e. W -> ph ) ) <-> ( x e. V -> A. y ( y e. W -> ph ) ) )
7	6	bicomi	|- ( ( x e. V -> A. y ( y e. W -> ph ) ) <-> A. y ( x e. V -> ( y e. W -> ph ) ) )
8	7	albii	|- ( A. x ( x e. V -> A. y ( y e. W -> ph ) ) <-> A. x A. y ( x e. V -> ( y e. W -> ph ) ) )
9		impexp	|- ( ( ( x e. V /\ y e. W ) -> ph ) <-> ( x e. V -> ( y e. W -> ph ) ) )
10		eleq1	|- ( x = A -> ( x e. V <-> A e. V ) )
11		eleq1	|- ( y = B -> ( y e. W <-> B e. W ) )
12	10 11	bi2anan9	|- ( ( x = A /\ y = B ) -> ( ( x e. V /\ y e. W ) <-> ( A e. V /\ B e. W ) ) )
13	12 1	imbi12d	|- ( ( x = A /\ y = B ) -> ( ( ( x e. V /\ y e. W ) -> ph ) <-> ( ( A e. V /\ B e. W ) -> ps ) ) )
14	9 13	bitr3id	|- ( ( x = A /\ y = B ) -> ( ( x e. V -> ( y e. W -> ph ) ) <-> ( ( A e. V /\ B e. W ) -> ps ) ) )
15	14	spc2gv	|- ( ( A e. V /\ B e. W ) -> ( A. x A. y ( x e. V -> ( y e. W -> ph ) ) -> ( ( A e. V /\ B e. W ) -> ps ) ) )
16	15	pm2.43a	|- ( ( A e. V /\ B e. W ) -> ( A. x A. y ( x e. V -> ( y e. W -> ph ) ) -> ps ) )
17	8 16	biimtrid	|- ( ( A e. V /\ B e. W ) -> ( A. x ( x e. V -> A. y ( y e. W -> ph ) ) -> ps ) )
18	5 17	biimtrid	|- ( ( A e. V /\ B e. W ) -> ( A. x ( x e. V -> A. y e. W ph ) -> ps ) )
19	2 18	biimtrid	|- ( ( A e. V /\ B e. W ) -> ( A. x e. V A. y e. W ph -> ps ) )