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

Metamath Proof Explorer

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