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 x=yxy
Assertion bj-dtrucor2v φ¬φ

Proof

Step Hyp Ref Expression
1 bj-dtrucor2v.1 x=yxy
2 ax6ev xx=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 ¬xx=y
7 2 6 pm2.24ii φ¬φ