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

Theorem elab 2915
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 2914 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1685   {cab 2270   _Vcvv 2789
This theorem is referenced by:  ralab  2927  rexab  2929  intab  3893  dfiin2g  3937  uniuni  4526  finds  4681  finds2  4683  opeliunxp  4739  funcnvuni  5283  fun11iun  5459  elabrex  5727  abrexco  5728  tfrlem3  6389  mapval2  6793  sbthlem2  6968  ssenen  7031  dffi2  7172  dffi3  7180  tctr  7421  tcmin  7422  tc2  7423  tz9.13  7459  tcrank  7550  kardex  7560  karden  7561  cardf2  7572  cardiun  7611  alephval3  7733  dfac3  7744  dfac5lem3  7748  dfac5lem4  7749  dfac2  7753  kmlem12  7783  cardcf  7874  cfeq0  7878  cfsuc  7879  cff1  7880  cflim2  7885  cfss  7887  axdc3lem2  8073  axdc3lem3  8074  axdclem  8142  brdom7disj  8152  brdom6disj  8153  tskuni  8401  gruina  8436  nqpr  8634  supmul  9718  dfnn2  9755  dfuzi  10098  seqof  11099  hashfacen  11388  hashf1lem1  11389  hashf1lem2  11390  shftfval  11561  infcvgaux1i  12311  efgrelexlemb  15055  lss1d  15716  lidldvgen  16003  zndvds  16499  cmpsublem  17122  cmpsub  17123  ptpjopn  17302  ptclsg  17305  txdis1cn  17325  tx1stc  17340  hauspwpwf1  17678  divstgplem  17799  i1fadd  19046  i1fmul  19047  i1fmulc  19054  mpfind  19424  pf1ind  19434  nmosetn0  21337  nmoolb  21343  nmlno0lem  21365  nmopsetn0  22441  nmfnsetn0  22454  nmoplb  22483  nmfnlb  22500  nmlnop0iALT  22571  nmopun  22590  nmcexi  22602  branmfn  22681  pjnmopi  22724  derangenlem  23109  dfrtrcl2  23452  dfon2lem3  23545  dfon2lem7  23549  fnimage  23878  imageval  23879  elo  24451  valcurfn  24614  intopcoaconlem3b  24949  intopcoaconlem3  24950  qusp  24953  dfiunv2  25327  cndpv  25460  pgapspf  25463  bhp2a  25587  sdclem2  25863  sdclem1  25864  heibor1lem  25944  eldiophss  26265  setindtrs  26529  hbtlem2  26739  hbtlem5  26743  rngunsnply  26789  psgnvali  26842  glbconxN  28846  pmapglbx  29237  dvhb1dimN  30454
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791
  Copyright terms: Public domain W3C validator