Metamath Proof Explorer


Theorem cbvral2

Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v . (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 cbvral2 x A y B φ z A w B ψ

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 _ z B
8 7 1 nfral z y B φ
9 nfcv _ x B
10 9 2 nfral x y B χ
11 5 ralbidv x = z y B φ y B χ
12 8 10 11 cbvralw x A y B φ z A y B χ
13 3 4 6 cbvralw y B χ w B ψ
14 13 ralbii z A y B χ z A w B ψ
15 12 14 bitri x A y B φ z A w B ψ