Theorem bj-hbnaeb

Description: Biconditional version of hbnae (to replace it?). (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-hbnaeb	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		hbnae	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )
2		sp	⊢ ( ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
3	1 2	impbii	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )