Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of Quine p. 44. (Contributed by NM, 1Aug1994)
Ref  Expression  

Hypotheses  elab.1   A e. _V 

elab.2   ( x = A > ( ph <> ps ) ) 

Assertion  elab   ( A e. { x  ph } <> ps ) 
Step  Hyp  Ref  Expression 

1  elab.1   A e. _V 

2  elab.2   ( x = A > ( ph <> ps ) ) 

3  nfv   F/ x ps 

4  3 1 2  elabf   ( A e. { x  ph } <> ps ) 