Theorem elab 3250

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   {cab 2452   _Vcvv 3113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115

This theorem is referenced by:  ralab  3264  rexab  3266  intab  4312  dfiin2g  4358  dfiunv2  4361  opeliunxp  5051  elabrex  6143  abrexco  6144  uniuni  6593  finds  6710  finds2  6712  funcnvuni  6737  fun11iun  6744  mapval2  7448  sbthlem2  7628  ssenen  7691  dffi2  7883  dffi3  7891  tctr  8171  tcmin  8172  tc2  8173  tz9.13  8209  tcrank  8302  kardex  8312  karden  8313  cardf2  8324  cardiun  8363  alephval3  8491  dfac3  8502  dfac5lem3  8506  dfac5lem4  8507  dfac2  8511  kmlem12  8541  cardcf  8632  cfeq0  8636  cfsuc  8637  cff1  8638  cflim2  8643  cfss  8645  axdc3lem2  8831  axdc3lem3  8832  axdclem  8899  brdom7disj  8909  brdom6disj  8910  tskuni  9161  gruina  9196  nqpr  9392  supmul  10511  dfnn2  10549  dfuzi  10951  seqof  12132  hashfacen  12469  hashf1lem1  12470  hashf1lem2  12471  0csh0  12727  shftfval  12866  infcvgaux1i  13631  symg1bas  16226  pmtrprfvalrn  16319  psgnvali  16339  efgrelexlemb  16574  lss1d  17409  lidldvgen  17702  mpfind  18004  pf1ind  18190  zndvds  18383  cmpsublem  19693  cmpsub  19694  ptpjopn  19876  ptclsg  19879  txdis1cn  19899  tx1stc  19914  hauspwpwf1  20251  divstgplem  20382  ustn0  20486  i1fadd  21865  i1fmul  21866  i1fmulc  21873  2wot2wont  24590  2spot2iun2spont  24595  rusgranumwlkb0  24657  usg2spot2nb  24770  nmosetn0  25384  nmoolb  25390  nmlno0lem  25412  nmopsetn0  26488  nmfnsetn0  26501  nmoplb  26530  nmfnlb  26547  nmlnop0iALT  26618  nmopun  26637  nmcexi  26649  branmfn  26728  pjnmopi  26771  fpwrelmapffslem  27255  esumc  27730  orvcval2  28065  derangenlem  28283  dfrtrcl2  28574  dfon2lem3  28822  dfon2lem7  28826  fnimage  29184  imageval  29185  supadd  29647  mblfinlem3  29658  mblfinlem4  29659  ismblfin  29660  itg2addnc  29674  sdclem2  29866  sdclem1  29867  heibor1lem  29936  eldiophss  30340  setindtrs  30599  hbtlem2  30705  hbtlem5  30709  rngunsnply  30755  nzss  30850  fourierdlem36  31471  fourierdlem54  31489  opeliun2xp  32018  glbconxN  34192  pmapglbx  34583  dvhb1dimN  35800