This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Theorem nf5
Description: Alternate definition of df-nf . (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 11-Sep-2021)
|
|
Ref |
Expression |
|
Assertion |
nf5 |
⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-nf |
⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ) |
| 2 |
|
nfa1 |
⊢ Ⅎ 𝑥 ∀ 𝑥 𝜑 |
| 3 |
2
|
19.23 |
⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ) |
| 4 |
1 3
|
bitr4i |
⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ) |