Theorem cbvrex2

Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v . (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	cbvrex2	|- ( E. x e. A E. y e. B ph <-> E. z e. A E. 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	nfrex	|- F/ z E. y e. B ph
9		nfcv	|- F/_ x B
10	9 2	nfrex	|- F/ x E. y e. B ch
11	5	rexbidv	|- ( x = z -> ( E. y e. B ph <-> E. y e. B ch ) )
12	8 10 11	cbvrexw	|- ( E. x e. A E. y e. B ph <-> E. z e. A E. y e. B ch )
13	3 4 6	cbvrexw	|- ( E. y e. B ch <-> E. w e. B ps )
14	13	rexbii	|- ( E. z e. A E. y e. B ch <-> E. z e. A E. w e. B ps )
15	12 14	bitri	|- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps )