Theorem elab 3246

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
elab.2

Assertion

Ref	Expression
elab

Distinct variable groups:   ,   ,

Proof of Theorem elab

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		elab.1	. 2
3		elab.2	. 2
4	1, 2, 3	elabf 3245	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442  cvv 3109

This theorem is referenced by:  ralab  3260  rexab  3262  intab  4317  dfiin2g  4363  dfiunv2  4366  opeliunxp  5056  elabrex  6155  abrexco  6156  uniuni  6609  finds  6726  finds2  6728  funcnvuni  6753  fun11iun  6760  mapval2  7468  sbthlem2  7648  ssenen  7711  dffi2  7903  dffi3  7911  tctr  8192  tcmin  8193  tc2  8194  tz9.13  8230  tcrank  8323  kardex  8333  karden  8334  cardf2  8345  cardiun  8384  alephval3  8512  dfac3  8523  dfac5lem3  8527  dfac5lem4  8528  dfac2  8532  kmlem12  8562  cardcf  8653  cfeq0  8657  cfsuc  8658  cff1  8659  cflim2  8664  cfss  8666  axdc3lem2  8852  axdc3lem3  8853  axdclem  8920  brdom7disj  8930  brdom6disj  8931  tskuni  9182  gruina  9217  nqpr  9413  supmul  10536  dfnn2  10574  dfuzi  10978  seqof  12164  hashfacen  12503  hashf1lem1  12504  hashf1lem2  12505  0csh0  12764  shftfval  12903  infcvgaux1i  13668  symg1bas  16421  pmtrprfvalrn  16513  psgnvali  16533  efgrelexlemb  16768  lss1d  17609  lidldvgen  17903  mpfind  18205  pf1ind  18391  zndvds  18588  cmpsublem  19899  cmpsub  19900  ptpjopn  20113  ptclsg  20116  txdis1cn  20136  tx1stc  20151  hauspwpwf1  20488  qustgplem  20619  ustn0  20723  i1fadd  22102  i1fmul  22103  i1fmulc  22110  2wot2wont  24886  2spot2iun2spont  24891  rusgranumwlkb0  24953  usg2spot2nb  25065  nmosetn0  25680  nmoolb  25686  nmlno0lem  25708  nmopsetn0  26784  nmfnsetn0  26797  nmoplb  26826  nmfnlb  26843  nmlnop0iALT  26914  nmopun  26933  nmcexi  26945  branmfn  27024  pjnmopi  27067  fpwrelmapffslem  27555  ldlfcntref  27857  esumc  28062  orvcval2  28397  derangenlem  28615  mclsssvlem  28922  mclsind  28930  dfrtrcl2  29071  dfon2lem3  29217  dfon2lem7  29221  fnimage  29579  imageval  29580  supadd  30042  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnc  30069  sdclem2  30235  sdclem1  30236  heibor1lem  30305  eldiophss  30708  setindtrs  30967  hbtlem2  31073  hbtlem5  31077  rngunsnply  31122  nzss  31222  upbdrech  31505  fourierdlem36  31925  opeliun2xp  32922  glbconxN  35102  pmapglbx  35493  dvhb1dimN  36712  trclub  37784  trclubg  37785  dfhe3  37799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111