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

Theorem elab 3025
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 3024 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1717   {cab 2373   _Vcvv 2899
This theorem is referenced by:  ralab  3038  rexab  3040  intab  4022  dfiin2g  4066  uniuni  4656  finds  4811  finds2  4813  opeliunxp  4869  funcnvuni  5458  fun11iun  5635  elabrex  5924  abrexco  5925  tfrlem3  6574  mapval2  6979  sbthlem2  7154  ssenen  7217  dffi2  7363  dffi3  7371  tctr  7612  tcmin  7613  tc2  7614  tz9.13  7650  tcrank  7741  kardex  7751  karden  7752  cardf2  7763  cardiun  7802  alephval3  7924  dfac3  7935  dfac5lem3  7939  dfac5lem4  7940  dfac2  7944  kmlem12  7974  cardcf  8065  cfeq0  8069  cfsuc  8070  cff1  8071  cflim2  8076  cfss  8078  axdc3lem2  8264  axdc3lem3  8265  axdclem  8332  brdom7disj  8342  brdom6disj  8343  tskuni  8591  gruina  8626  nqpr  8824  supmul  9908  dfnn2  9945  dfuzi  10292  seqof  11307  hashfacen  11630  hashf1lem1  11631  hashf1lem2  11632  shftfval  11812  infcvgaux1i  12563  efgrelexlemb  15309  lss1d  15966  lidldvgen  16253  zndvds  16753  cmpsublem  17384  cmpsub  17385  ptpjopn  17565  ptclsg  17568  txdis1cn  17588  tx1stc  17603  hauspwpwf1  17940  divstgplem  18071  ustn0  18171  i1fadd  19454  i1fmul  19455  i1fmulc  19462  mpfind  19832  pf1ind  19842  nmosetn0  22114  nmoolb  22120  nmlno0lem  22142  nmopsetn0  23216  nmfnsetn0  23229  nmoplb  23258  nmfnlb  23275  nmlnop0iALT  23346  nmopun  23365  nmcexi  23377  branmfn  23456  pjnmopi  23499  esumc  24242  orvcval2  24495  derangenlem  24636  dfrtrcl2  24927  dfon2lem3  25165  dfon2lem7  25169  fnimage  25492  imageval  25493  supadd  25948  itg2addnc  25959  sdclem2  26137  sdclem1  26138  heibor1lem  26209  eldiophss  26524  setindtrs  26787  hbtlem2  26997  hbtlem5  27001  rngunsnply  27047  psgnvali  27100  glbconxN  29492  pmapglbx  29883  dvhb1dimN  31100
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 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901
  Copyright terms: Public domain W3C validator