Theorem wl-cbvalnaed

Description: wl-cbvalnae with a context. (Contributed by Wolf Lammen, 28-Jul-2019)

	Ref	Expression
Hypotheses	wl-cbvalnaed.1	$$⊢Ⅎx\phi$$
	wl-cbvalnaed.2	$$⊢Ⅎy\phi$$
	wl-cbvalnaed.3	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎy\psi \right)$$
	wl-cbvalnaed.4	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎx\chi \right)$$
	wl-cbvalnaed.5	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
Assertion	wl-cbvalnaed	$$⊢\phi \to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-cbvalnaed.1	$$⊢Ⅎx\phi$$
2		wl-cbvalnaed.2	$$⊢Ⅎy\phi$$
3		wl-cbvalnaed.3	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎy\psi \right)$$
4		wl-cbvalnaed.4	$$⊢\phi \to \left(\neg \forall xx=y\to Ⅎx\chi \right)$$
5		wl-cbvalnaed.5	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
6	1 2 5	wl-dral1d	$$⊢\phi \to \left(\forall xx=y\to \left(\forall x\psi \leftrightarrow \forall y\chi \right)\right)$$
7	6	imp	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$
8		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
9	1 8	nfan	$$⊢Ⅎx\left(\phi \wedge \neg \forall xx=y\right)$$
10		wl-nfnae1	$$⊢Ⅎy\neg \forall xx=y$$
11	2 10	nfan	$$⊢Ⅎy\left(\phi \wedge \neg \forall xx=y\right)$$
12	3	imp	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎy\psi$$
13	4	imp	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\chi$$
14	5	adantr	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
15	9 11 12 13 14	cbv2	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$
16	7 15	pm2.61dan	$$⊢\phi \to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$