Description: Nonfreeness implies the equivalent of ax-5 . See nf5r . (Contributed by BJ, 28-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nnfa | ⊢ ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bj-nnf | ⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) | |
2 | 1 | simprbi | ⊢ ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) ) |