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\to \neg \forall y\neg y=x$$

Proof

Step	Hyp	Ref	Expression
1		ax6v	$$⊢\neg \forall y\neg y=x$$
2	1	a1i	$$⊢x=x\to \neg \forall y\neg y=x$$