This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nf5-1

Description: One direction of nf5 can be proved with a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 16-Sep-2021)

Ref Expression
Assertion nf5-1 ⊢ ∀ x φ → ∀ x φ → Ⅎ x φ

Proof

Step Hyp Ref Expression
1 exim ⊢ ∀ x φ → ∀ x φ → ∃ x φ → ∃ x ∀ x φ
2 hbe1a ⊢ ∃ x ∀ x φ → ∀ x φ
3 1 2 syl6 ⊢ ∀ x φ → ∀ x φ → ∃ x φ → ∀ x φ
4 3 nfd ⊢ ∀ x φ → ∀ x φ → Ⅎ x φ