Theorem elab 3217

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

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   e. wcel 1872   {cab 2407   _Vcvv 3080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082

This theorem is referenced by:  ralab  3231  rexab  3233  intab  4286  dfiin2g  4332  dfiunv2  4335  opeliunxp  4905  elabrex  6164  abrexco  6165  uniuni  6615  finds  6734  finds2  6736  funcnvuni  6761  fun11iun  6768  mapval2  7513  sbthlem2  7693  ssenen  7756  dffi2  7947  dffi3  7955  tctr  8233  tcmin  8234  tc2  8235  tz9.13  8271  tcrank  8364  kardex  8374  karden  8375  cardf2  8386  cardiun  8425  alephval3  8549  dfac3  8560  dfac5lem3  8564  dfac5lem4  8565  dfac2  8569  kmlem12  8599  cardcf  8690  cfeq0  8694  cfsuc  8695  cff1  8696  cflim2  8701  cfss  8703  axdc3lem2  8889  axdc3lem3  8890  axdclem  8957  brdom7disj  8967  brdom6disj  8968  tskuni  9216  gruina  9251  nqpr  9447  supadd  10583  supmul  10587  dfnn2  10630  dfuzi  11034  seqof  12277  hashfacen  12622  hashf1lem1  12623  hashf1lem2  12624  0csh0  12898  trclun  13079  dfrtrcl2  13126  shftfval  13134  infcvgaux1i  13915  symg1bas  17037  pmtrprfvalrn  17129  psgnvali  17149  efgrelexlemb  17400  lss1d  18186  lidldvgen  18479  mpfind  18759  pf1ind  18943  zndvds  19119  cmpsublem  20413  cmpsub  20414  ptpjopn  20626  ptclsg  20629  txdis1cn  20649  tx1stc  20664  hauspwpwf1  21001  qustgplem  21134  ustn0  21234  i1fadd  22652  i1fmul  22653  i1fmulc  22660  2wot2wont  25613  2spot2iun2spont  25618  rusgranumwlkb0  25680  usg2spot2nb  25792  nmosetn0  26405  nmoolb  26411  nmlno0lem  26433  nmopsetn0  27517  nmfnsetn0  27530  nmoplb  27559  nmfnlb  27576  nmlnop0iALT  27647  nmopun  27666  nmcexi  27678  branmfn  27757  pjnmopi  27800  fpwrelmapffslem  28324  ldlfcntref  28690  esumc  28881  orvcval2  29300  derangenlem  29903  mclsssvlem  30209  mclsind  30217  dfon2lem3  30439  dfon2lem7  30443  fnimage  30702  imageval  30703  poimirlem4  31909  poimirlem5  31910  poimirlem6  31911  poimirlem7  31912  poimirlem8  31913  poimirlem9  31914  poimirlem10  31915  poimirlem11  31916  poimirlem12  31917  poimirlem13  31918  poimirlem14  31919  poimirlem15  31920  poimirlem16  31921  poimirlem17  31922  poimirlem18  31923  poimirlem19  31924  poimirlem20  31925  poimirlem21  31926  poimirlem22  31927  poimirlem25  31930  poimirlem26  31931  poimirlem27  31932  poimirlem29  31934  poimirlem31  31936  mblfinlem3  31944  mblfinlem4  31945  ismblfin  31946  itg2addnc  31961  sdclem2  32036  sdclem1  32037  heibor1lem  32106  glbconxN  32913  pmapglbx  33304  dvhb1dimN  34523  eldiophss  35587  setindtrs  35851  hbtlem2  35954  hbtlem5  35958  rngunsnply  36010  dftrcl3  36283  brtrclfv2  36290  dfrtrcl3  36296  dfhe3  36341  nzss  36637  upbdrech  37478  fourierdlem36  37947  sge0resplit  38157  hoidmvlelem1  38322  ausgrusgri  39071  usgredgedga  39112  opeliun2xp  39765