Metamath Proof Explorer


Theorem nf5ri

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 15-Mar-2023)

Ref Expression
Hypothesis nf5ri.1 𝑥 𝜑
Assertion nf5ri ( 𝜑 → ∀ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 nf5ri.1 𝑥 𝜑
2 1 nfri ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 )
3 2 19.23bi ( 𝜑 → ∀ 𝑥 𝜑 )