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\phi$$
	cbvral2.2	$$⊢Ⅎx\chi$$
	cbvral2.3	$$⊢Ⅎw\chi$$
	cbvral2.4	$$⊢Ⅎy\psi$$
	cbvral2.5	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
	cbvral2.6	$$⊢y=w\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	cbvral2	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall z\in A\forall w\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvral2.1	$$⊢Ⅎz\phi$$
2		cbvral2.2	$$⊢Ⅎx\chi$$
3		cbvral2.3	$$⊢Ⅎw\chi$$
4		cbvral2.4	$$⊢Ⅎy\psi$$
5		cbvral2.5	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
6		cbvral2.6	$$⊢y=w\to \left(\chi \leftrightarrow \psi \right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}zB$$
8	7 1	nfral	$$⊢Ⅎz\forall y\in B\phi$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
10	9 2	nfral	$$⊢Ⅎx\forall y\in B\chi$$
11	5	ralbidv	$$⊢x=z\to \left(\forall y\in B\phi \leftrightarrow \forall y\in B\chi \right)$$
12	8 10 11	cbvralw	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall z\in A\forall y\in B\chi$$
13	3 4 6	cbvralw	$$⊢\forall y\in B\chi \leftrightarrow \forall w\in B\psi$$
14	13	ralbii	$$⊢\forall z\in A\forall y\in B\chi \leftrightarrow \forall z\in A\forall w\in B\psi$$
15	12 14	bitri	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall z\in A\forall w\in B\psi$$