Theorem cbvralf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvralf.1	|- F/_ x A
	cbvralf.2	|- F/_ y A
	cbvralf.3	|- F/ y ph
	cbvralf.4	|- F/ x ps
	cbvralf.5	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvralf	|- ( A. x e. A ph <-> A. y e. A ps )

Proof

Step	Hyp	Ref	Expression
1		cbvralf.1	|- F/_ x A
2		cbvralf.2	|- F/_ y A
3		cbvralf.3	|- F/ y ph
4		cbvralf.4	|- F/ x ps
5		cbvralf.5	|- ( x = y -> ( ph <-> ps ) )
6		nfv	|- F/ z ( x e. A -> ph )
7	1	nfcri	|- F/ x z e. A
8		nfs1v	|- F/ x [ z / x ] ph
9	7 8	nfim	|- F/ x ( z e. A -> [ z / x ] ph )
10		eleq1w	|- ( x = z -> ( x e. A <-> z e. A ) )
11		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
12	10 11	imbi12d	|- ( x = z -> ( ( x e. A -> ph ) <-> ( z e. A -> [ z / x ] ph ) ) )
13	6 9 12	cbvalv1	|- ( A. x ( x e. A -> ph ) <-> A. z ( z e. A -> [ z / x ] ph ) )
14	2	nfcri	|- F/ y z e. A
15	3	nfsb	|- F/ y [ z / x ] ph
16	14 15	nfim	|- F/ y ( z e. A -> [ z / x ] ph )
17		nfv	|- F/ z ( y e. A -> ps )
18		eleq1w	|- ( z = y -> ( z e. A <-> y e. A ) )
19		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
20	4 5	sbie	|- ( [ y / x ] ph <-> ps )
21	19 20	bitrdi	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
22	18 21	imbi12d	|- ( z = y -> ( ( z e. A -> [ z / x ] ph ) <-> ( y e. A -> ps ) ) )
23	16 17 22	cbvalv1	|- ( A. z ( z e. A -> [ z / x ] ph ) <-> A. y ( y e. A -> ps ) )
24	13 23	bitri	|- ( A. x ( x e. A -> ph ) <-> A. y ( y e. A -> ps ) )
25		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
26		df-ral	|- ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
27	24 25 26	3bitr4i	|- ( A. x e. A ph <-> A. y e. A ps )