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 -> ( ph <-> ch ) )
	cbvral2v.2	|- ( y = w -> ( ch <-> ps ) )
Assertion	cbvral2v	|- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )

Proof

Step	Hyp	Ref	Expression
1		cbvral2v.1	|- ( x = z -> ( ph <-> ch ) )
2		cbvral2v.2	|- ( y = w -> ( ch <-> ps ) )
3	1	ralbidv	|- ( x = z -> ( A. y e. B ph <-> A. y e. B ch ) )
4	3	cbvralv	|- ( A. x e. A A. y e. B ph <-> A. z e. A A. y e. B ch )
5	2	cbvralv	|- ( A. y e. B ch <-> A. w e. B ps )
6	5	ralbii	|- ( A. z e. A A. y e. B ch <-> A. z e. A A. w e. B ps )
7	4 6	bitri	|- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )