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

Metamath Proof Explorer

Theorem nfrd

Description: Consequence of the definition of not-free in a context. (Contributed by Wolf Lammen, 15-Oct-2021)

Ref Expression
Hypothesis nfrd.1 ⊢ φ → Ⅎ x ψ
Assertion nfrd ⊢ φ → ∃ x ψ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 nfrd.1 ⊢ φ → Ⅎ x ψ
2 df-nf ⊢ Ⅎ x ψ ↔ ∃ x ψ → ∀ x ψ
3 1 2 sylib ⊢ φ → ∃ x ψ → ∀ x ψ