Metamath Proof Explorer


Theorem cbvrex2

Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Hypotheses cbvral2.1 zφ
cbvral2.2 xχ
cbvral2.3 wχ
cbvral2.4 yψ
cbvral2.5 x=zφχ
cbvral2.6 y=wχψ
Assertion cbvrex2 xAyBφzAwBψ

Proof

Step Hyp Ref Expression
1 cbvral2.1 zφ
2 cbvral2.2 xχ
3 cbvral2.3 wχ
4 cbvral2.4 yψ
5 cbvral2.5 x=zφχ
6 cbvral2.6 y=wχψ
7 nfcv _zB
8 7 1 nfrex zyBφ
9 nfcv _xB
10 9 2 nfrex xyBχ
11 5 rexbidv x=zyBφyBχ
12 8 10 11 cbvrexw xAyBφzAyBχ
13 3 4 6 cbvrexw yBχwBψ
14 13 rexbii zAyBχzAwBψ
15 12 14 bitri xAyBφzAwBψ