This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝑥 = 𝑦 → 𝑥 ≠ 𝑦 )
	Assertion	bj-dtrucor2v	⊢ ( 𝜑 ∧ ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bj-dtrucor2v.1	⊢ ( 𝑥 = 𝑦 → 𝑥 ≠ 𝑦 )
2		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑦
3	1	necon2bi	⊢ ( 𝑥 = 𝑦 → ¬ 𝑥 = 𝑦 )
4		pm2.01	⊢ ( ( 𝑥 = 𝑦 → ¬ 𝑥 = 𝑦 ) → ¬ 𝑥 = 𝑦 )
5	3 4	ax-mp	⊢ ¬ 𝑥 = 𝑦
6	5	nex	⊢ ¬ ∃ 𝑥 𝑥 = 𝑦
7	2 6	pm2.24ii	⊢ ( 𝜑 ∧ ¬ 𝜑 )