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

Theorem elab 2914
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 1605 . 2  |-  F/ x ps
2 elab.1 . 2  |-  A  e. 
_V
3 elab.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabf 2913 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   {cab 2269   _Vcvv 2788
This theorem is referenced by:  ralab  2926  rexab  2928  intab  3892  dfiin2g  3936  uniuni  4527  finds  4682  finds2  4684  opeliunxp  4740  funcnvuni  5317  fun11iun  5493  elabrex  5765  abrexco  5766  tfrlem3  6393  mapval2  6797  sbthlem2  6972  ssenen  7035  dffi2  7176  dffi3  7184  tctr  7425  tcmin  7426  tc2  7427  tz9.13  7463  tcrank  7554  kardex  7564  karden  7565  cardf2  7576  cardiun  7615  alephval3  7737  dfac3  7748  dfac5lem3  7752  dfac5lem4  7753  dfac2  7757  kmlem12  7787  cardcf  7878  cfeq0  7882  cfsuc  7883  cff1  7884  cflim2  7889  cfss  7891  axdc3lem2  8077  axdc3lem3  8078  axdclem  8146  brdom7disj  8156  brdom6disj  8157  tskuni  8405  gruina  8440  nqpr  8638  supmul  9722  dfnn2  9759  dfuzi  10102  seqof  11103  hashfacen  11392  hashf1lem1  11393  hashf1lem2  11394  shftfval  11565  infcvgaux1i  12315  efgrelexlemb  15059  lss1d  15720  lidldvgen  16007  zndvds  16503  cmpsublem  17126  cmpsub  17127  ptpjopn  17306  ptclsg  17309  txdis1cn  17329  tx1stc  17344  hauspwpwf1  17682  divstgplem  17803  i1fadd  19050  i1fmul  19051  i1fmulc  19058  mpfind  19428  pf1ind  19438  nmosetn0  21343  nmoolb  21349  nmlno0lem  21371  nmopsetn0  22445  nmfnsetn0  22458  nmoplb  22487  nmfnlb  22504  nmlnop0iALT  22575  nmopun  22594  nmcexi  22606  branmfn  22685  pjnmopi  22728  orvcval2  23659  derangenlem  23702  dfrtrcl2  24045  dfon2lem3  24141  dfon2lem7  24145  fnimage  24468  imageval  24469  elo  25041  valcurfn  25203  intopcoaconlem3b  25538  intopcoaconlem3  25539  qusp  25542  dfiunv2  25916  cndpv  26049  pgapspf  26052  bhp2a  26176  sdclem2  26452  sdclem1  26453  heibor1lem  26533  eldiophss  26854  setindtrs  27118  hbtlem2  27328  hbtlem5  27332  rngunsnply  27378  psgnvali  27431  glbconxN  29567  pmapglbx  29958  dvhb1dimN  31175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790
  Copyright terms: Public domain W3C validator