Theorem cbvral2v

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 cbvral2vw when possible. (Contributed by NM, 10-Aug-2004) (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	cbvral2v	$$⊢\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		cbvral2v.1	$$⊢x=z\to \left(\phi \leftrightarrow \chi \right)$$
2		cbvral2v.2	$$⊢y=w\to \left(\chi \leftrightarrow \psi \right)$$
3	1	ralbidv	$$⊢x=z\to \left(\forall y\in B\phi \leftrightarrow \forall y\in B\chi \right)$$
4	3	cbvralv	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall z\in A\forall y\in B\chi$$
5	2	cbvralv	$$⊢\forall y\in B\chi \leftrightarrow \forall w\in B\psi$$
6	5	ralbii	$$⊢\forall z\in A\forall y\in B\chi \leftrightarrow \forall z\in A\forall w\in B\psi$$
7	4 6	bitri	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall z\in A\forall w\in B\psi$$