Theorem elab 3042

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

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721   {cab 2390   _Vcvv 2916

This theorem is referenced by:  ralab  3055  rexab  3057  intab  4040  dfiin2g  4084  dfiunv2  4087  uniuni  4675  finds  4830  finds2  4832  opeliunxp  4888  funcnvuni  5477  fun11iun  5654  elabrex  5944  abrexco  5945  tfrlem3  6597  mapval2  7002  sbthlem2  7177  ssenen  7240  dffi2  7386  dffi3  7394  tctr  7635  tcmin  7636  tc2  7637  tz9.13  7673  tcrank  7764  kardex  7774  karden  7775  cardf2  7786  cardiun  7825  alephval3  7947  dfac3  7958  dfac5lem3  7962  dfac5lem4  7963  dfac2  7967  kmlem12  7997  cardcf  8088  cfeq0  8092  cfsuc  8093  cff1  8094  cflim2  8099  cfss  8101  axdc3lem2  8287  axdc3lem3  8288  axdclem  8355  brdom7disj  8365  brdom6disj  8366  tskuni  8614  gruina  8649  nqpr  8847  supmul  9932  dfnn2  9969  dfuzi  10316  seqof  11335  hashfacen  11658  hashf1lem1  11659  hashf1lem2  11660  shftfval  11840  infcvgaux1i  12591  efgrelexlemb  15337  lss1d  15994  lidldvgen  16281  zndvds  16785  cmpsublem  17416  cmpsub  17417  ptpjopn  17597  ptclsg  17600  txdis1cn  17620  tx1stc  17635  hauspwpwf1  17972  divstgplem  18103  ustn0  18203  i1fadd  19540  i1fmul  19541  i1fmulc  19548  mpfind  19918  pf1ind  19928  nmosetn0  22219  nmoolb  22225  nmlno0lem  22247  nmopsetn0  23321  nmfnsetn0  23334  nmoplb  23363  nmfnlb  23380  nmlnop0iALT  23451  nmopun  23470  nmcexi  23482  branmfn  23561  pjnmopi  23604  esumc  24399  orvcval2  24669  derangenlem  24810  dfrtrcl2  25101  dfon2lem3  25355  dfon2lem7  25359  fnimage  25682  imageval  25683  supadd  26138  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnc  26158  sdclem2  26336  sdclem1  26337  heibor1lem  26408  eldiophss  26723  setindtrs  26986  hbtlem2  27196  hbtlem5  27200  rngunsnply  27246  psgnvali  27299  2wot2wont  28083  2spot2iun2spont  28088  usg2spot2nb  28168  glbconxN  29860  pmapglbx  30251  dvhb1dimN  31468

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918