Metamath Proof Explorer


Theorem nfra1

Description: The setvar x is not free in A. x e. A ph . (Contributed by NM, 18-Oct-1996) (Revised by Mario Carneiro, 7-Oct-2016)

Ref Expression
Assertion nfra1 xxAφ

Proof

Step Hyp Ref Expression
1 df-ral xAφxxAφ
2 nfa1 xxxAφ
3 1 2 nfxfr xxAφ