Theorem cbvrex2vw

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v with a disjoint variable condition, which does not require ax-13 . (Contributed by FL, 2-Jul-2012) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvrex2vw.1	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
	cbvrex2vw.2	$$⊢y=w\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	cbvrex2vw	$$⊢\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		cbvrex2vw.1	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
2		cbvrex2vw.2	$$⊢y=w\to \left(\chi \leftrightarrow \psi \right)$$
3	1	rexbidv	$$⊢x=z\to \left(\exists y\in B\phi \leftrightarrow \exists y\in B\chi \right)$$
4	3	cbvrexvw	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists z\in A\exists y\in B\chi$$
5	2	cbvrexvw	$$⊢\exists y\in B\chi \leftrightarrow \exists w\in B\psi$$
6	5	rexbii	$$⊢\exists z\in A\exists y\in B\chi \leftrightarrow \exists z\in A\exists w\in B\psi$$
7	4 6	bitri	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists z\in A\exists w\in B\psi$$