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	$$⊢\forall x\in A\phi \to \forall x\forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfra1	$$⊢Ⅎx\forall x\in A\phi$$
2	1	nf5ri	$$⊢\forall x\in A\phi \to \forall x\forall x\in A\phi$$