Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10Oct2016)
Ref  Expression  

Hypothesis  nfeq1.1   F/_ x A 

Assertion  nfel1   F/ x A e. B 
Step  Hyp  Ref  Expression 

1  nfeq1.1   F/_ x A 

2  nfcv   F/_ x B 

3  1 2  nfel   F/ x A e. B 