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	⊢ ( 𝑥 = 𝑥 → ¬ ∀ 𝑦 ¬ 𝑦 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		ax6v	⊢ ¬ ∀ 𝑦 ¬ 𝑦 = 𝑥
2	1	a1i	⊢ ( 𝑥 = 𝑥 → ¬ ∀ 𝑦 ¬ 𝑦 = 𝑥 )