Metamath Proof Explorer


Theorem bj-nnfa

Description: Nonfreeness implies the equivalent of ax-5 . See nf5r . (Contributed by BJ, 28-Jul-2023)

Ref Expression
Assertion bj-nnfa ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-bj-nnf ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) )
2 1 simprbi ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )