Theorem bj-alnnf

Description: In deduction-style proofs, it is equivalent to assert that the context holds for all values of a variable, or that is does not depend on that variable. (Contributed by BJ, 28-Mar-2026)

	Ref	Expression
Assertion	bj-alnnf	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜑 → Ⅎ' 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( 𝜑 → ( ∃ 𝑥 𝜑 → 𝜑 ) )
2	1	biantrur	⊢ ( ( 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) ) ↔ ( ( 𝜑 → ( ∃ 𝑥 𝜑 → 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) )
3		pm5.4	⊢ ( ( 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) ) ↔ ( 𝜑 → ∀ 𝑥 𝜑 ) )
4		pm4.76	⊢ ( ( ( 𝜑 → ( ∃ 𝑥 𝜑 → 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) ↔ ( 𝜑 → ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) )
5	2 3 4	3bitr3i	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜑 → ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) )
6		df-bj-nnf	⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) )
7	6	imbi2i	⊢ ( ( 𝜑 → Ⅎ' 𝑥 𝜑 ) ↔ ( 𝜑 → ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) )
8	5 7	bitr4i	⊢ ( ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( 𝜑 → Ⅎ' 𝑥 𝜑 ) )