Metamath Proof Explorer

Theorem nfab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Assertion nfab1 
|- F/_ x { x | ph }

Proof

Step Hyp Ref Expression
1 nfsab1 
 |-  F/ x y e. { x | ph }
2 1 nfci 
 |-  F/_ x { x | ph }