Theorem cbvalw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		cbvalw.1	|- ( A. x ph -> A. y A. x ph )
2		cbvalw.2	|- ( -. ps -> A. x -. ps )
3		cbvalw.3	|- ( A. y ps -> A. x A. y ps )
4		cbvalw.4	|- ( -. ph -> A. y -. ph )
5		cbvalw.5	|- ( x = y -> ( ph <-> ps ) )
6	5	biimpd	|- ( x = y -> ( ph -> ps ) )
7	1 2 6	cbvaliw	|- ( A. x ph -> A. y ps )
8	5	biimprd	|- ( x = y -> ( ps -> ph ) )
9	8	equcoms	|- ( y = x -> ( ps -> ph ) )
10	3 4 9	cbvaliw	|- ( A. y ps -> A. x ph )
11	7 10	impbii	|- ( A. x ph <-> A. y ps )