Theorem bj-hbntbi

Description: Strengthening hbnt by replacing its consequent with a biconditional. See also hbntg and hbntal . (Contributed by BJ, 20-Oct-2019) Proved from bj-19.9htbi . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-hbntbi	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ¬ 𝜑 ↔ ∀ 𝑥 ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-19.9htbi	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 ↔ 𝜑 ) )
2	1	bicomd	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( 𝜑 ↔ ∃ 𝑥 𝜑 ) )
3	2	notbid	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 ) )
4		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
5	3 4	bitr4di	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ¬ 𝜑 ↔ ∀ 𝑥 ¬ 𝜑 ) )