Theorem elab 3095

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1362   e. wcel 1755   {cab 2419   _Vcvv 2962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964

This theorem is referenced by:  ralab  3109  rexab  3111  intab  4146  dfiin2g  4191  dfiunv2  4194  opeliunxp  4877  elabrex  5947  abrexco  5948  uniuni  6374  finds  6491  finds2  6493  funcnvuni  6519  fun11iun  6526  mapval2  7230  sbthlem2  7410  ssenen  7473  dffi2  7661  dffi3  7669  tctr  7948  tcmin  7949  tc2  7950  tz9.13  7986  tcrank  8079  kardex  8089  karden  8090  cardf2  8101  cardiun  8140  alephval3  8268  dfac3  8279  dfac5lem3  8283  dfac5lem4  8284  dfac2  8288  kmlem12  8318  cardcf  8409  cfeq0  8413  cfsuc  8414  cff1  8415  cflim2  8420  cfss  8422  axdc3lem2  8608  axdc3lem3  8609  axdclem  8676  brdom7disj  8686  brdom6disj  8687  tskuni  8938  gruina  8973  nqpr  9171  supmul  10286  dfnn2  10323  dfuzi  10720  seqof  11847  hashfacen  12191  hashf1lem1  12192  hashf1lem2  12193  0csh0  12414  shftfval  12543  infcvgaux1i  13302  symg1bas  15881  pmtrprfvalrn  15974  psgnvali  15994  efgrelexlemb  16227  lss1d  16966  lidldvgen  17259  zndvds  17824  cmpsublem  18844  cmpsub  18845  ptpjopn  19027  ptclsg  19030  txdis1cn  19050  tx1stc  19065  hauspwpwf1  19402  divstgplem  19533  ustn0  19637  i1fadd  21015  i1fmul  21016  i1fmulc  21023  mpfind  21396  pf1ind  21406  nmosetn0  23988  nmoolb  23994  nmlno0lem  24016  nmopsetn0  25092  nmfnsetn0  25105  nmoplb  25134  nmfnlb  25151  nmlnop0iALT  25222  nmopun  25241  nmcexi  25253  branmfn  25332  pjnmopi  25375  fpwrelmapffslem  25857  esumc  26359  orvcval2  26689  derangenlem  26907  dfrtrcl2  27197  dfon2lem3  27445  dfon2lem7  27449  fnimage  27807  imageval  27808  supadd  28262  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  itg2addnc  28290  sdclem2  28482  sdclem1  28483  heibor1lem  28552  eldiophss  28958  setindtrs  29219  hbtlem2  29325  hbtlem5  29329  rngunsnply  29375  2wot2wont  30251  2spot2iun2spont  30256  rusgranumwlkb0  30417  usg2spot2nb  30504  opeliun2xp  30565  glbconxN  32595  pmapglbx  32986  dvhb1dimN  34203