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 
|- F/ x A. x e. A ph

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2 nfa1 
 |-  F/ x A. x ( x e. A -> ph )
3 1 2 nfxfr 
 |-  F/ x A. x e. A ph