Theorem cbvalvOLD

Description: Obsolete version of cbvalv as of 11-Sep-2023. (Contributed by NM, 5-Aug-1993) Remove dependency on ax-10 . (Revised by Wolf Lammen, 17-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cbvalv.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvalvOLD	|- ( A. x ph <-> A. y ps )

Proof

Step	Hyp	Ref	Expression
1		cbvalv.1	|- ( x = y -> ( ph <-> ps ) )
2		ax-5	|- ( ph -> A. y ph )
3	2	hbal	|- ( A. x ph -> A. y A. x ph )
4	1	spv	|- ( A. x ph -> ps )
5	3 4	alrimih	|- ( A. x ph -> A. y ps )
6		ax-5	|- ( ps -> A. x ps )
7	6	hbal	|- ( A. y ps -> A. x A. y ps )
8	1	equcoms	|- ( y = x -> ( ph <-> ps ) )
9	8	bicomd	|- ( y = x -> ( ps <-> ph ) )
10	9	spv	|- ( A. y ps -> ph )
11	7 10	alrimih	|- ( A. y ps -> A. x ph )
12	5 11	impbii	|- ( A. x ph <-> A. y ps )