Theorem bj-denot 34782

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

Assertion

Ref	Expression
bj-denot	⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥)

Distinct variable group:   𝑥,𝑦

Proof of Theorem bj-denot

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-6 1972

This theorem is referenced by: (None)