Theorem cbvral3v

Description: Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvral3vw when possible. (Contributed by NM, 10-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvral3v.1	|- ( x = w -> ( ph <-> ch ) )
	cbvral3v.2	|- ( y = v -> ( ch <-> th ) )
	cbvral3v.3	|- ( z = u -> ( th <-> ps ) )
Assertion	cbvral3v	|- ( A. x e. A A. y e. B A. z e. C ph <-> A. w e. A A. v e. B A. u e. C ps )

Proof

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