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

Theorem elab 3075
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 1629 . 2  |-  F/ x ps
2 elab.1 . 2  |-  A  e. 
_V
3 elab.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabf 3074 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {cab 2422   _Vcvv 2949
This theorem is referenced by:  ralab  3088  rexab  3090  intab  4073  dfiin2g  4117  dfiunv2  4120  uniuni  4709  finds  4864  finds2  4866  opeliunxp  4922  funcnvuni  5511  fun11iun  5688  elabrex  5978  abrexco  5979  tfrlem3  6631  mapval2  7036  sbthlem2  7211  ssenen  7274  dffi2  7421  dffi3  7429  tctr  7672  tcmin  7673  tc2  7674  tz9.13  7710  tcrank  7801  kardex  7811  karden  7812  cardf2  7823  cardiun  7862  alephval3  7984  dfac3  7995  dfac5lem3  7999  dfac5lem4  8000  dfac2  8004  kmlem12  8034  cardcf  8125  cfeq0  8129  cfsuc  8130  cff1  8131  cflim2  8136  cfss  8138  axdc3lem2  8324  axdc3lem3  8325  axdclem  8392  brdom7disj  8402  brdom6disj  8403  tskuni  8651  gruina  8686  nqpr  8884  supmul  9969  dfnn2  10006  dfuzi  10353  seqof  11373  hashfacen  11696  hashf1lem1  11697  hashf1lem2  11698  shftfval  11878  infcvgaux1i  12629  efgrelexlemb  15375  lss1d  16032  lidldvgen  16319  zndvds  16823  cmpsublem  17455  cmpsub  17456  ptpjopn  17637  ptclsg  17640  txdis1cn  17660  tx1stc  17675  hauspwpwf1  18012  divstgplem  18143  ustn0  18243  i1fadd  19580  i1fmul  19581  i1fmulc  19588  mpfind  19958  pf1ind  19968  nmosetn0  22259  nmoolb  22265  nmlno0lem  22287  nmopsetn0  23361  nmfnsetn0  23374  nmoplb  23403  nmfnlb  23420  nmlnop0iALT  23491  nmopun  23510  nmcexi  23522  branmfn  23601  pjnmopi  23644  esumc  24439  orvcval2  24709  derangenlem  24850  dfrtrcl2  25141  dfon2lem3  25405  dfon2lem7  25409  fnimage  25767  imageval  25768  supadd  26230  mblfinlem2  26236  mblfinlem3  26237  ismblfin  26238  itg2addnc  26250  sdclem2  26438  sdclem1  26439  heibor1lem  26510  eldiophss  26825  setindtrs  27088  hbtlem2  27297  hbtlem5  27301  rngunsnply  27347  psgnvali  27400  2wot2wont  28307  2spot2iun2spont  28312  usg2spot2nb  28392  glbconxN  30113  pmapglbx  30504  dvhb1dimN  31721
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951
  Copyright terms: Public domain W3C validator