Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvelimf-o.1	$$⊢\phi \to \forall x\phi$$
	dvelimf-o.2	$$⊢\psi \to \forall z\psi$$
	dvelimf-o.3	$$⊢z=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	dvelimf-o	$$⊢\neg \forall xx=y\to \left(\psi \to \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dvelimf-o.1	$$⊢\phi \to \forall x\phi$$
2		dvelimf-o.2	$$⊢\psi \to \forall z\psi$$
3		dvelimf-o.3	$$⊢z=y\to \left(\phi \leftrightarrow \psi \right)$$
4		hba1-o	$$⊢\forall z\left(z=y\to \phi \right)\to \forall z\forall z\left(z=y\to \phi \right)$$
5		ax-c11	$$⊢\forall zz=x\to \left(\forall z\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)$$
6	5	aecoms-o	$$⊢\forall xx=z\to \left(\forall z\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)$$
7	4 6	syl5	$$⊢\forall xx=z\to \left(\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)$$
8	7	a1d	$$⊢\forall xx=z\to \left(\neg \forall xx=y\to \left(\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)\right)$$
9		hbnae-o	$$⊢\neg \forall xx=z\to \forall z\neg \forall xx=z$$
10		hbnae-o	$$⊢\neg \forall xx=y\to \forall z\neg \forall xx=y$$
11	9 10	hban	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to \forall z\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)$$
12		hbnae-o	$$⊢\neg \forall xx=z\to \forall x\neg \forall xx=z$$
13		hbnae-o	$$⊢\neg \forall xx=y\to \forall x\neg \forall xx=y$$
14	12 13	hban	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to \forall x\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)$$
15		ax-c9	$$⊢\neg \forall xx=z\to \left(\neg \forall xx=y\to \left(z=y\to \forall xz=y\right)\right)$$
16	15	imp	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to \left(z=y\to \forall xz=y\right)$$
17	1	a1i	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to \left(\phi \to \forall x\phi \right)$$
18	14 16 17	hbimd	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to \left(\left(z=y\to \phi \right)\to \forall x\left(z=y\to \phi \right)\right)$$
19	11 18	hbald	$$⊢\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\to \left(\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)$$
20	19	ex	$$⊢\neg \forall xx=z\to \left(\neg \forall xx=y\to \left(\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)\right)$$
21	8 20	pm2.61i	$$⊢\neg \forall xx=y\to \left(\forall z\left(z=y\to \phi \right)\to \forall x\forall z\left(z=y\to \phi \right)\right)$$
22	2 3	equsalh	$$⊢\forall z\left(z=y\to \phi \right)\leftrightarrow \psi$$
23	22	albii	$$⊢\forall x\forall z\left(z=y\to \phi \right)\leftrightarrow \forall x\psi$$
24	21 22 23	3imtr3g	$$⊢\neg \forall xx=y\to \left(\psi \to \forall x\psi \right)$$