Theorem cbvalw

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

	Ref	Expression
Hypotheses	cbvalw.1	$$⊢\forall x\phi \to \forall y\forall x\phi$$
	cbvalw.2	$$⊢\neg \psi \to \forall x\neg \psi$$
	cbvalw.3	$$⊢\forall y\psi \to \forall x\forall y\psi$$
	cbvalw.4	$$⊢\neg \phi \to \forall y\neg \phi$$
	cbvalw.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvalw	$$⊢\forall x\phi \leftrightarrow \forall y\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvalw.1	$$⊢\forall x\phi \to \forall y\forall x\phi$$
2		cbvalw.2	$$⊢\neg \psi \to \forall x\neg \psi$$
3		cbvalw.3	$$⊢\forall y\psi \to \forall x\forall y\psi$$
4		cbvalw.4	$$⊢\neg \phi \to \forall y\neg \phi$$
5		cbvalw.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
6	5	biimpd	$$⊢x=y\to \left(\phi \to \psi \right)$$
7	1 2 6	cbvaliw	$$⊢\forall x\phi \to \forall y\psi$$
8	5	biimprd	$$⊢x=y\to \left(\psi \to \phi \right)$$
9	8	equcoms	$$⊢y=x\to \left(\psi \to \phi \right)$$
10	3 4 9	cbvaliw	$$⊢\forall y\psi \to \forall x\phi$$
11	7 10	impbii	$$⊢\forall x\phi \leftrightarrow \forall y\psi$$