Theorem elab 3197

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   e. wcel 1898   {cab 2448   _Vcvv 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059

This theorem is referenced by:  ralab  3211  rexab  3213  intab  4279  dfiin2g  4325  dfiunv2  4328  opeliunxp  4908  elabrex  6178  abrexco  6179  uniuni  6632  finds  6751  finds2  6753  funcnvuni  6778  fun11iun  6785  mapval2  7532  sbthlem2  7714  ssenen  7777  dffi2  7968  dffi3  7976  tctr  8255  tcmin  8256  tc2  8257  tz9.13  8293  tcrank  8386  kardex  8396  karden  8397  cardf2  8408  cardiun  8447  alephval3  8572  dfac3  8583  dfac5lem3  8587  dfac5lem4  8588  dfac2  8592  kmlem12  8622  cardcf  8713  cfeq0  8717  cfsuc  8718  cff1  8719  cflim2  8724  cfss  8726  axdc3lem2  8912  axdc3lem3  8913  axdclem  8980  brdom7disj  8990  brdom6disj  8991  tskuni  9239  gruina  9274  nqpr  9470  supadd  10608  supmul  10612  dfnn2  10655  dfuzi  11060  seqof  12308  hashfacen  12656  hashf1lem1  12657  hashf1lem2  12658  0csh0  12938  trclun  13133  dfrtrcl2  13180  shftfval  13188  infcvgaux1i  13970  symg1bas  17092  pmtrprfvalrn  17184  psgnvali  17204  efgrelexlemb  17455  lss1d  18241  lidldvgen  18534  mpfind  18814  pf1ind  18998  zndvds  19175  cmpsublem  20469  cmpsub  20470  ptpjopn  20682  ptclsg  20685  txdis1cn  20705  tx1stc  20720  hauspwpwf1  21057  qustgplem  21190  ustn0  21290  i1fadd  22709  i1fmul  22710  i1fmulc  22717  2wot2wont  25670  2spot2iun2spont  25675  rusgranumwlkb0  25737  usg2spot2nb  25849  nmosetn0  26462  nmoolb  26468  nmlno0lem  26490  nmopsetn0  27574  nmfnsetn0  27587  nmoplb  27616  nmfnlb  27633  nmlnop0iALT  27704  nmopun  27723  nmcexi  27735  branmfn  27814  pjnmopi  27857  fpwrelmapffslem  28369  ldlfcntref  28732  esumc  28923  orvcval2  29341  derangenlem  29944  mclsssvlem  30250  mclsind  30258  dfon2lem3  30481  dfon2lem7  30485  fnimage  30746  imageval  30747  poimirlem4  31990  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem9  31995  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem29  32015  poimirlem31  32017  mblfinlem3  32025  mblfinlem4  32026  ismblfin  32027  itg2addnc  32042  sdclem2  32117  sdclem1  32118  heibor1lem  32187  glbconxN  32989  pmapglbx  33380  dvhb1dimN  34599  eldiophss  35663  setindtrs  35926  hbtlem2  36029  hbtlem5  36033  rngunsnply  36085  dftrcl3  36358  brtrclfv2  36365  dfrtrcl3  36371  dfhe3  36416  nzss  36711  upbdrech  37598  fourierdlem36  38107  sge0resplit  38351  hoidmvlelem1  38524  ausgrusgri  39399  ushgredgedga  39452  ushgredgedgaloop  39454  opeliun2xp  40483