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 
|- ( A. x e. A ph -> A. x A. x e. A ph )

Proof

Step Hyp Ref Expression
1 nfra1 
 |-  F/ x A. x e. A ph
2 1 nf5ri 
 |-  ( A. x e. A ph -> A. x A. x e. A ph )