Theorem elab 3224

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

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   e. wcel 1870   {cab 2414   _Vcvv 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089

This theorem is referenced by:  ralab  3238  rexab  3240  intab  4289  dfiin2g  4335  dfiunv2  4338  opeliunxp  4906  elabrex  6163  abrexco  6164  uniuni  6614  finds  6733  finds2  6735  funcnvuni  6760  fun11iun  6767  mapval2  7509  sbthlem2  7689  ssenen  7752  dffi2  7943  dffi3  7951  tctr  8223  tcmin  8224  tc2  8225  tz9.13  8261  tcrank  8354  kardex  8364  karden  8365  cardf2  8376  cardiun  8415  alephval3  8539  dfac3  8550  dfac5lem3  8554  dfac5lem4  8555  dfac2  8559  kmlem12  8589  cardcf  8680  cfeq0  8684  cfsuc  8685  cff1  8686  cflim2  8691  cfss  8693  axdc3lem2  8879  axdc3lem3  8880  axdclem  8947  brdom7disj  8957  brdom6disj  8958  tskuni  9207  gruina  9242  nqpr  9438  supadd  10575  supmul  10579  dfnn2  10622  dfuzi  11026  seqof  12267  hashfacen  12612  hashf1lem1  12613  hashf1lem2  12614  0csh0  12880  trclun  13057  dfrtrcl2  13104  shftfval  13112  infcvgaux1i  13893  symg1bas  16988  pmtrprfvalrn  17080  psgnvali  17100  efgrelexlemb  17335  lss1d  18121  lidldvgen  18414  mpfind  18694  pf1ind  18878  zndvds  19051  cmpsublem  20345  cmpsub  20346  ptpjopn  20558  ptclsg  20561  txdis1cn  20581  tx1stc  20596  hauspwpwf1  20933  qustgplem  21066  ustn0  21166  i1fadd  22530  i1fmul  22531  i1fmulc  22538  2wot2wont  25459  2spot2iun2spont  25464  rusgranumwlkb0  25526  usg2spot2nb  25638  nmosetn0  26251  nmoolb  26257  nmlno0lem  26279  nmopsetn0  27353  nmfnsetn0  27366  nmoplb  27395  nmfnlb  27412  nmlnop0iALT  27483  nmopun  27502  nmcexi  27514  branmfn  27593  pjnmopi  27636  fpwrelmapffslem  28160  ldlfcntref  28520  esumc  28711  orvcval2  29117  derangenlem  29682  mclsssvlem  29988  mclsind  29996  dfon2lem3  30218  dfon2lem7  30222  fnimage  30481  imageval  30482  poimirlem4  31648  poimirlem5  31649  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem9  31653  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem13  31657  poimirlem14  31658  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem29  31673  poimirlem31  31675  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  itg2addnc  31700  sdclem2  31775  sdclem1  31776  heibor1lem  31845  glbconxN  32652  pmapglbx  33043  dvhb1dimN  34262  eldiophss  35326  setindtrs  35586  hbtlem2  35689  hbtlem5  35693  rngunsnply  35738  dftrcl3  35951  brtrclfv2  35958  dfrtrcl3  35964  dfhe3  36007  nzss  36303  upbdrech  37132  fourierdlem36  37574  sge0resplit  37782  opeliun2xp  38874