Theorem cbvralfwOLD

Description: Obsolete version of cbvralfw as of 23-May-2024. (Contributed by NM, 7-Mar-2004) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralfwOLD.1	|- F/_ x A
2		cbvralfwOLD.2	|- F/_ y A
3		cbvralfwOLD.3	|- F/ y ph
4		cbvralfwOLD.4	|- F/ x ps
5		cbvralfwOLD.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	nfsbv	|- 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	sbiev	|- ( [ 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 )