Theorem gencbval

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996)

	Ref	Expression
Hypotheses	gencbval.1	$$⊢A\in \mathrm{V}$$
	gencbval.2	$$⊢A=y\to \left(\phi \leftrightarrow \psi \right)$$
	gencbval.3	$$⊢A=y\to \left(\chi \leftrightarrow \theta \right)$$
	gencbval.4	$$⊢\theta \leftrightarrow \exists x\left(\chi \wedge A=y\right)$$
Assertion	gencbval	$$⊢\forall x\left(\chi \to \phi \right)\leftrightarrow \forall y\left(\theta \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		gencbval.1	$$⊢A\in \mathrm{V}$$
2		gencbval.2	$$⊢A=y\to \left(\phi \leftrightarrow \psi \right)$$
3		gencbval.3	$$⊢A=y\to \left(\chi \leftrightarrow \theta \right)$$
4		gencbval.4	$$⊢\theta \leftrightarrow \exists x\left(\chi \wedge A=y\right)$$
5	2	notbid	$$⊢A=y\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
6	1 5 3 4	gencbvex	$$⊢\exists x\left(\chi \wedge \neg \phi \right)\leftrightarrow \exists y\left(\theta \wedge \neg \psi \right)$$
7		exanali	$$⊢\exists x\left(\chi \wedge \neg \phi \right)\leftrightarrow \neg \forall x\left(\chi \to \phi \right)$$
8		exanali	$$⊢\exists y\left(\theta \wedge \neg \psi \right)\leftrightarrow \neg \forall y\left(\theta \to \psi \right)$$
9	6 7 8	3bitr3i	$$⊢\neg \forall x\left(\chi \to \phi \right)\leftrightarrow \neg \forall y\left(\theta \to \psi \right)$$
10	9	con4bii	$$⊢\forall x\left(\chi \to \phi \right)\leftrightarrow \forall y\left(\theta \to \psi \right)$$