Theorem elab 3127

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   e. wcel 1756   {cab 2429   _Vcvv 2993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995

This theorem is referenced by:  ralab  3141  rexab  3143  intab  4179  dfiin2g  4224  dfiunv2  4227  opeliunxp  4911  elabrex  5981  abrexco  5982  uniuni  6406  finds  6523  finds2  6525  funcnvuni  6551  fun11iun  6558  mapval2  7263  sbthlem2  7443  ssenen  7506  dffi2  7694  dffi3  7702  tctr  7981  tcmin  7982  tc2  7983  tz9.13  8019  tcrank  8112  kardex  8122  karden  8123  cardf2  8134  cardiun  8173  alephval3  8301  dfac3  8312  dfac5lem3  8316  dfac5lem4  8317  dfac2  8321  kmlem12  8351  cardcf  8442  cfeq0  8446  cfsuc  8447  cff1  8448  cflim2  8453  cfss  8455  axdc3lem2  8641  axdc3lem3  8642  axdclem  8709  brdom7disj  8719  brdom6disj  8720  tskuni  8971  gruina  9006  nqpr  9204  supmul  10319  dfnn2  10356  dfuzi  10753  seqof  11884  hashfacen  12228  hashf1lem1  12229  hashf1lem2  12230  0csh0  12451  shftfval  12580  infcvgaux1i  13340  symg1bas  15922  pmtrprfvalrn  16015  psgnvali  16035  efgrelexlemb  16268  lss1d  17066  lidldvgen  17359  mpfind  17644  pf1ind  17811  zndvds  18004  cmpsublem  19024  cmpsub  19025  ptpjopn  19207  ptclsg  19210  txdis1cn  19230  tx1stc  19245  hauspwpwf1  19582  divstgplem  19713  ustn0  19817  i1fadd  21195  i1fmul  21196  i1fmulc  21203  nmosetn0  24187  nmoolb  24193  nmlno0lem  24215  nmopsetn0  25291  nmfnsetn0  25304  nmoplb  25333  nmfnlb  25350  nmlnop0iALT  25421  nmopun  25440  nmcexi  25452  branmfn  25531  pjnmopi  25574  fpwrelmapffslem  26054  esumc  26527  orvcval2  26863  derangenlem  27081  dfrtrcl2  27372  dfon2lem3  27620  dfon2lem7  27624  fnimage  27982  imageval  27983  supadd  28444  mblfinlem3  28456  mblfinlem4  28457  ismblfin  28458  itg2addnc  28472  sdclem2  28664  sdclem1  28665  heibor1lem  28734  eldiophss  29139  setindtrs  29400  hbtlem2  29506  hbtlem5  29510  rngunsnply  29556  2wot2wont  30431  2spot2iun2spont  30436  rusgranumwlkb0  30597  usg2spot2nb  30684  opeliun2xp  30746  glbconxN  33118  pmapglbx  33509  dvhb1dimN  34726