Theorem elab 2918

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 1552	. 2 |- F/ x ps
2		elab.1	. 2 |- A e. _V
3		elab.2	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	elabf 2917	1 |- ( A e. { x | ph } <-> ps )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   e. wcel 2177   {cab 2192   _Vcvv 2773

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775

This theorem is referenced by:  ralab  2934  rexab  2936  intab  3916  dfiin2g  3962  dfiunv2  3965  uniuni  4502  dcextest  4633  peano5  4650  finds  4652  finds2  4653  funcnvuni  5348  fun11iun  5550  elabrex  5833  abrexco  5835  mapval2  6772  ssenen  6955  snexxph  7059  sbthlem2  7067  indpi  7462  nqprm  7662  nqprrnd  7663  nqprdisj  7664  nqprloc  7665  nqprl  7671  nqpru  7672  cauappcvgprlem2  7780  caucvgprlem2  7800  peano1nnnn  7972  peano2nnnn  7973  1nn  9054  peano2nn  9055  dfuzi  9490  hashfacen  10988  shftfvalg  11173  ovshftex  11174  shftfval  11176  4sqlemafi  12762  lss1d  14189  txdis1cn  14794  bj-ssom  15946