Theorem bj-dfnnf3

Description: Alternate definition of nonfreeness when sp is available. (Contributed by BJ, 28-Jul-2023) The proof should not rely on df-nf . (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bj-nnfea	⊢ ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
2		bj-19.21bit	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑥 𝜑 → 𝜑 ) )
3		bj-19.23bit	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) → ( 𝜑 → ∀ 𝑥 𝜑 ) )
4		df-bj-nnf	⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) )
5	2 3 4	sylanbrc	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) → Ⅎ' 𝑥 𝜑 )
6	1 5	impbii	⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )