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\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	cbvrex2	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists z\in A\exists 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	nfrexw	$$⊢Ⅎz\exists y\in B\phi$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
10	9 2	nfrexw	$$⊢Ⅎx\exists y\in B\chi$$
11	5	rexbidv	$$⊢x=z\to \left(\exists y\in B\phi \leftrightarrow \exists y\in B\chi \right)$$
12	8 10 11	cbvrexw	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists z\in A\exists y\in B\chi$$
13	3 4 6	cbvrexw	$$⊢\exists y\in B\chi \leftrightarrow \exists w\in B\psi$$
14	13	rexbii	$$⊢\exists z\in A\exists y\in B\chi \leftrightarrow \exists z\in A\exists w\in B\psi$$
15	12 14	bitri	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists z\in A\exists w\in B\psi$$