Theorem elab 3350

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202

This theorem is referenced by:  ralab  3367  rexab  3369  intab  4507  dfiin2g  4553  dfiunv2  4556  opeliunxp  5170  elabrex  6501  abrexco  6502  uniuni  6971  finds  7092  finds2  7094  funcnvuni  7119  fun11iun  7126  mapval2  7887  sbthlem2  8071  ssenen  8134  dffi2  8329  dffi3  8337  tctr  8616  tcmin  8617  tc2  8618  tz9.13  8654  tcrank  8747  kardex  8757  karden  8758  cardf2  8769  cardiun  8808  alephval3  8933  dfac3  8944  dfac5lem3  8948  dfac5lem4  8949  dfac2  8953  kmlem12  8983  cardcf  9074  cfeq0  9078  cfsuc  9079  cff1  9080  cflim2  9085  cfss  9087  axdc3lem2  9273  axdc3lem3  9274  axdclem  9341  brdom7disj  9353  brdom6disj  9354  tskuni  9605  gruina  9640  nqpr  9836  supadd  10991  supmul  10995  dfnn2  11033  dfuzi  11468  seqof  12858  hashfacen  13238  hashf1lem1  13239  hashf1lem2  13240  0csh0  13539  trclun  13755  dfrtrcl2  13802  shftfval  13810  infcvgaux1i  14589  symg1bas  17816  pmtrprfvalrn  17908  psgnvali  17928  efgrelexlemb  18163  lss1d  18963  lidldvgen  19255  mpfind  19536  pf1ind  19719  zndvds  19898  cmpsublem  21202  cmpsub  21203  ptpjopn  21415  ptclsg  21418  txdis1cn  21438  tx1stc  21453  hauspwpwf1  21791  qustgplem  21924  ustn0  22024  i1fadd  23462  i1fmul  23463  i1fmulc  23470  ausgrusgri  26063  ushgredgedg  26121  ushgredgedgloop  26123  wspniunwspnon  26819  rusgrnumwwlkb0  26866  fusgr2wsp2nb  27198  nmosetn0  27620  nmoolb  27626  nmlno0lem  27648  nmopsetn0  28724  nmfnsetn0  28737  nmoplb  28766  nmfnlb  28783  nmlnop0iALT  28854  nmopun  28873  nmcexi  28885  branmfn  28964  pjnmopi  29007  fpwrelmapffslem  29507  ldlfcntref  29921  esumc  30113  orvcval2  30520  derangenlem  31153  mclsssvlem  31459  mclsind  31467  dfon2lem3  31690  dfon2lem7  31694  nosupno  31849  nosupbnd1lem1  31854  fnimage  32036  imageval  32037  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnc  33464  sdclem2  33538  sdclem1  33539  heibor1lem  33608  glbconxN  34664  pmapglbx  35055  dvhb1dimN  36274  eldiophss  37338  setindtrs  37592  hbtlem2  37694  hbtlem5  37698  rngunsnply  37743  dftrcl3  38012  brtrclfv2  38019  dfrtrcl3  38025  dfhe3  38069  nzss  38516  upbdrech  39519  fourierdlem36  40360  sge0resplit  40623  hoidmvlelem1  40809  elsprel  41725  opeliun2xp  42111  setrec2lem1  42440