Theorem elab 2951

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.)

Hypotheses

Ref	Expression
elab.1	|- A e. _V
elab.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
elab	|- ( A e. { x | ph } <-> ps )

Distinct variable groups:   ps, x   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem elab

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 |- F/ x ps
2		elab.1	. 2 |- A e. _V
3		elab.2	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	elabf 2950	1 |- ( A e. { x | ph } <-> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2202   {cab 2217   _Vcvv 2803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805

This theorem is referenced by:  ralab  2967  rexab  2969  intab  3962  dfiin2g  4008  dfiunv2  4011  uniuni  4554  dcextest  4685  peano5  4702  finds  4704  finds2  4705  funcnvuni  5406  fun11iun  5613  elabrex  5908  abrexco  5910  mapval2  6890  ssenen  7080  snexxph  7192  sbthlem2  7200  indpi  7605  nqprm  7805  nqprrnd  7806  nqprdisj  7807  nqprloc  7808  nqprl  7814  nqpru  7815  cauappcvgprlem2  7923  caucvgprlem2  7943  peano1nnnn  8115  peano2nnnn  8116  1nn  9197  peano2nn  9198  dfuzi  9633  hashfacen  11144  shftfvalg  11439  ovshftex  11440  shftfval  11442  4sqlemafi  13029  lss1d  14459  txdis1cn  15069  ushgredgedg  16147  ushgredgedgloop  16149  bj-ssom  16632