Theorem bj-dtrucor2v

Description: Version of dtrucor2 with a disjoint variable condition, which does not require ax-13 (nor ax-4 , ax-5 , ax-7 , ax-12 ). (Contributed by BJ, 16-Jul-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-dtrucor2v.1	$$⊢x=y\to x\ne y$$
Assertion	bj-dtrucor2v	$$⊢\left(\phi \wedge \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-dtrucor2v.1	$$⊢x=y\to x\ne y$$
2		ax6ev	$$⊢\exists xx=y$$
3	1	necon2bi	$$⊢x=y\to \neg x=y$$
4		pm2.01	$$⊢\left(x=y\to \neg x=y\right)\to \neg x=y$$
5	3 4	ax-mp	$$⊢\neg x=y$$
6	5	nex	$$⊢\neg \exists xx=y$$
7	2 6	pm2.24ii	$$⊢\left(\phi \wedge \neg \phi \right)$$