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) (Revised by Gino Giotto, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvrex2vw.1	|- ( x = z -> ( ph <-> ch ) )
	cbvrex2vw.2	|- ( y = w -> ( ch <-> ps ) )
Assertion	cbvrex2vw	|- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps )

Proof

Step	Hyp	Ref	Expression
1		cbvrex2vw.1	|- ( x = z -> ( ph <-> ch ) )
2		cbvrex2vw.2	|- ( y = w -> ( ch <-> ps ) )
3	1	rexbidv	|- ( x = z -> ( E. y e. B ph <-> E. y e. B ch ) )
4	3	cbvrexvw	|- ( E. x e. A E. y e. B ph <-> E. z e. A E. y e. B ch )
5	2	cbvrexvw	|- ( E. y e. B ch <-> E. w e. B ps )
6	5	rexbii	|- ( E. z e. A E. y e. B ch <-> E. z e. A E. w e. B ps )
7	4 6	bitri	|- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps )