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=Ay=Bφψ
Assertion rspc2gv AVBWxVyWφψ

Proof

Step Hyp Ref Expression
1 rspc2gv.1 x=Ay=Bφψ
2 df-ral xVyWφxxVyWφ
3 df-ral yWφyyWφ
4 3 imbi2i xVyWφxVyyWφ
5 4 albii xxVyWφxxVyyWφ
6 19.21v yxVyWφxVyyWφ
7 6 bicomi xVyyWφyxVyWφ
8 7 albii xxVyyWφxyxVyWφ
9 impexp xVyWφxVyWφ
10 eleq1 x=AxVAV
11 eleq1 y=ByWBW
12 10 11 bi2anan9 x=Ay=BxVyWAVBW
13 12 1 imbi12d x=Ay=BxVyWφAVBWψ
14 9 13 bitr3id x=Ay=BxVyWφAVBWψ
15 14 spc2gv AVBWxyxVyWφAVBWψ
16 15 pm2.43a AVBWxyxVyWφψ
17 8 16 syl5bi AVBWxxVyyWφψ
18 5 17 syl5bi AVBWxxVyWφψ
19 2 18 syl5bi AVBWxVyWφψ