Metamath Proof Explorer

Theorem hbra1

Description: The setvar x is not free in A. x e. A ph . (Contributed by NM, 18-Oct-1996) (Proof shortened by Wolf Lammen, 7-Dec-2019)

Ref Expression
Assertion hbra1 ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜑
2 1 nf5ri ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜑 )