Theorem cbvral2

Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v . (Contributed by Alexander van der Vekens, 2-Jul-2017)

	Ref	Expression
Hypotheses	cbvral2.1	|- F/ z ph
	cbvral2.2	|- F/ x ch
	cbvral2.3	|- F/ w ch
	cbvral2.4	|- F/ y ps
	cbvral2.5	|- ( x = z -> ( ph <-> ch ) )
	cbvral2.6	|- ( y = w -> ( ch <-> ps ) )
Assertion	cbvral2	|- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )

Proof

Step	Hyp	Ref	Expression
1		cbvral2.1	|- F/ z ph
2		cbvral2.2	|- F/ x ch
3		cbvral2.3	|- F/ w ch
4		cbvral2.4	|- F/ y ps
5		cbvral2.5	|- ( x = z -> ( ph <-> ch ) )
6		cbvral2.6	|- ( y = w -> ( ch <-> ps ) )
7		nfcv	|- F/_ z B
8	7 1	nfral	|- F/ z A. y e. B ph
9		nfcv	|- F/_ x B
10	9 2	nfral	|- F/ x A. y e. B ch
11	5	ralbidv	|- ( x = z -> ( A. y e. B ph <-> A. y e. B ch ) )
12	8 10 11	cbvralw	|- ( A. x e. A A. y e. B ph <-> A. z e. A A. y e. B ch )
13	3 4 6	cbvralw	|- ( A. y e. B ch <-> A. w e. B ps )
14	13	ralbii	|- ( A. z e. A A. y e. B ch <-> A. z e. A A. w e. B ps )
15	12 14	bitri	|- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )