Theorem cbvrex2v

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrex2vw when possible. (Contributed by FL, 2-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvral2v.1	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
	cbvral2v.2	$$⊢y=w\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	cbvrex2v	$$⊢\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		cbvral2v.1	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
2		cbvral2v.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	cbvrexv	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists z\in A\exists y\in B\chi$$
5	2	cbvrexv	$$⊢\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$$