Metamath Proof Explorer


Theorem bj-denot

Description: A weakening of ax-6 and ax6v . (Contributed by BJ, 4-Apr-2021) (New usage is discouraged.)

Ref Expression
Assertion bj-denot x = x ¬ y ¬ y = x

Proof

Step Hyp Ref Expression
1 ax6v ¬ y ¬ y = x
2 1 a1i x = x ¬ y ¬ y = x