MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elab Unicode version

Theorem elab 3026
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
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ x ps
2 elab.1 . 2  |-  A  e. 
_V
3 elab.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabf 3025 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   {cab 2374   _Vcvv 2900
This theorem is referenced by:  ralab  3039  rexab  3041  intab  4023  dfiin2g  4067  uniuni  4657  finds  4812  finds2  4814  opeliunxp  4870  funcnvuni  5459  fun11iun  5636  elabrex  5925  abrexco  5926  tfrlem3  6575  mapval2  6980  sbthlem2  7155  ssenen  7218  dffi2  7364  dffi3  7372  tctr  7613  tcmin  7614  tc2  7615  tz9.13  7651  tcrank  7742  kardex  7752  karden  7753  cardf2  7764  cardiun  7803  alephval3  7925  dfac3  7936  dfac5lem3  7940  dfac5lem4  7941  dfac2  7945  kmlem12  7975  cardcf  8066  cfeq0  8070  cfsuc  8071  cff1  8072  cflim2  8077  cfss  8079  axdc3lem2  8265  axdc3lem3  8266  axdclem  8333  brdom7disj  8343  brdom6disj  8344  tskuni  8592  gruina  8627  nqpr  8825  supmul  9909  dfnn2  9946  dfuzi  10293  seqof  11308  hashfacen  11631  hashf1lem1  11632  hashf1lem2  11633  shftfval  11813  infcvgaux1i  12564  efgrelexlemb  15310  lss1d  15967  lidldvgen  16254  zndvds  16754  cmpsublem  17385  cmpsub  17386  ptpjopn  17566  ptclsg  17569  txdis1cn  17589  tx1stc  17604  hauspwpwf1  17941  divstgplem  18072  ustn0  18172  i1fadd  19455  i1fmul  19456  i1fmulc  19463  mpfind  19833  pf1ind  19843  nmosetn0  22115  nmoolb  22121  nmlno0lem  22143  nmopsetn0  23217  nmfnsetn0  23230  nmoplb  23259  nmfnlb  23276  nmlnop0iALT  23347  nmopun  23366  nmcexi  23378  branmfn  23457  pjnmopi  23500  esumc  24243  orvcval2  24496  derangenlem  24637  dfrtrcl2  24928  dfon2lem3  25166  dfon2lem7  25170  fnimage  25493  imageval  25494  supadd  25949  itg2addnc  25960  sdclem2  26138  sdclem1  26139  heibor1lem  26210  eldiophss  26525  setindtrs  26788  hbtlem2  26998  hbtlem5  27002  rngunsnply  27048  psgnvali  27101  glbconxN  29493  pmapglbx  29884  dvhb1dimN  31101
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902
  Copyright terms: Public domain W3C validator