Theorem cbv2OLD

Description: Obsolete version of cbv2 as of 10-Sep-2023. (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbv2OLD.1	|- F/ x ph
2		cbv2OLD.2	|- F/ y ph
3		cbv2OLD.3	|- ( ph -> F/ y ps )
4		cbv2OLD.4	|- ( ph -> F/ x ch )
5		cbv2OLD.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
6	2	nf5ri	|- ( ph -> A. y ph )
7	1 6	alrimi	|- ( ph -> A. x A. y ph )
8	3	nf5rd	|- ( ph -> ( ps -> A. y ps ) )
9	4	nf5rd	|- ( ph -> ( ch -> A. x ch ) )
10	8 9 5	cbv2h	|- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )
11	7 10	syl	|- ( ph -> ( A. x ps <-> A. y ch ) )