Theorem bj-dtru

Description: Remove dependency on ax-13 from dtru . (Contributed by BJ, 31-May-2019)

TODO: This predates the removal of ax-13 in dtru . But actually, sn-dtru is better than either, so move it to Main with sn-el (and determine whether bj-dtru should be kept as ALT or deleted).

(Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-dtru	$$⊢\neg \forall xx=y$$

Proof

Step	Hyp	Ref	Expression
1		el	$$⊢\exists wx\in w$$
2		ax-nul	$$⊢\exists z\forall x\neg x\in z$$
3		sp	$$⊢\forall x\neg x\in z\to \neg x\in z$$
4	2 3	eximii	$$⊢\exists z\neg x\in z$$
5		exdistrv	$$⊢\exists w\exists z\left(x\in w\wedge \neg x\in z\right)\leftrightarrow \left(\exists wx\in w\wedge \exists z\neg x\in z\right)$$
6	1 4 5	mpbir2an	$$⊢\exists w\exists z\left(x\in w\wedge \neg x\in z\right)$$
7		ax9	$$⊢w=z\to \left(x\in w\to x\in z\right)$$
8	7	com12	$$⊢x\in w\to \left(w=z\to x\in z\right)$$
9	8	con3dimp	$$⊢\left(x\in w\wedge \neg x\in z\right)\to \neg w=z$$
10	9	2eximi	$$⊢\exists w\exists z\left(x\in w\wedge \neg x\in z\right)\to \exists w\exists z\neg w=z$$
11	6 10	ax-mp	$$⊢\exists w\exists z\neg w=z$$
12		equequ2	$$⊢z=y\to \left(w=z\leftrightarrow w=y\right)$$
13	12	notbid	$$⊢z=y\to \left(\neg w=z\leftrightarrow \neg w=y\right)$$
14		ax7	$$⊢x=w\to \left(x=y\to w=y\right)$$
15	14	con3d	$$⊢x=w\to \left(\neg w=y\to \neg x=y\right)$$
16	15	spimevw	$$⊢\neg w=y\to \exists x\neg x=y$$
17	13 16	syl6bi	$$⊢z=y\to \left(\neg w=z\to \exists x\neg x=y\right)$$
18		ax7	$$⊢x=z\to \left(x=y\to z=y\right)$$
19	18	con3d	$$⊢x=z\to \left(\neg z=y\to \neg x=y\right)$$
20	19	spimevw	$$⊢\neg z=y\to \exists x\neg x=y$$
21	20	a1d	$$⊢\neg z=y\to \left(\neg w=z\to \exists x\neg x=y\right)$$
22	17 21	pm2.61i	$$⊢\neg w=z\to \exists x\neg x=y$$
23	22	exlimivv	$$⊢\exists w\exists z\neg w=z\to \exists x\neg x=y$$
24	11 23	ax-mp	$$⊢\exists x\neg x=y$$
25		exnal	$$⊢\exists x\neg x=y\leftrightarrow \neg \forall xx=y$$
26	24 25	mpbi	$$⊢\neg \forall xx=y$$