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 -> x =/= y )
Assertion	bj-dtrucor2v	|- ( ph /\ -. ph )

Proof

Step	Hyp	Ref	Expression
1		bj-dtrucor2v.1	|- ( x = y -> x =/= y )
2		ax6ev	|- E. x x = y
3	1	necon2bi	|- ( x = y -> -. x = y )
4		pm2.01	|- ( ( x = y -> -. x = y ) -> -. x = y )
5	3 4	ax-mp	|- -. x = y
6	5	nex	|- -. E. x x = y
7	2 6	pm2.24ii	|- ( ph /\ -. ph )