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

Theorem elab 2927
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 1609 . 2  |-  F/ x ps
2 elab.1 . 2  |-  A  e. 
_V
3 elab.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabf 2926 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   {cab 2282   _Vcvv 2801
This theorem is referenced by:  ralab  2939  rexab  2941  intab  3908  dfiin2g  3952  uniuni  4543  finds  4698  finds2  4700  opeliunxp  4756  funcnvuni  5333  fun11iun  5509  elabrex  5781  abrexco  5782  tfrlem3  6409  mapval2  6813  sbthlem2  6988  ssenen  7051  dffi2  7192  dffi3  7200  tctr  7441  tcmin  7442  tc2  7443  tz9.13  7479  tcrank  7570  kardex  7580  karden  7581  cardf2  7592  cardiun  7631  alephval3  7753  dfac3  7764  dfac5lem3  7768  dfac5lem4  7769  dfac2  7773  kmlem12  7803  cardcf  7894  cfeq0  7898  cfsuc  7899  cff1  7900  cflim2  7905  cfss  7907  axdc3lem2  8093  axdc3lem3  8094  axdclem  8162  brdom7disj  8172  brdom6disj  8173  tskuni  8421  gruina  8456  nqpr  8654  supmul  9738  dfnn2  9775  dfuzi  10118  seqof  11119  hashfacen  11408  hashf1lem1  11409  hashf1lem2  11410  shftfval  11581  infcvgaux1i  12331  efgrelexlemb  15075  lss1d  15736  lidldvgen  16023  zndvds  16519  cmpsublem  17142  cmpsub  17143  ptpjopn  17322  ptclsg  17325  txdis1cn  17345  tx1stc  17360  hauspwpwf1  17698  divstgplem  17819  i1fadd  19066  i1fmul  19067  i1fmulc  19074  mpfind  19444  pf1ind  19454  nmosetn0  21359  nmoolb  21365  nmlno0lem  21387  nmopsetn0  22461  nmfnsetn0  22474  nmoplb  22503  nmfnlb  22520  nmlnop0iALT  22591  nmopun  22610  nmcexi  22622  branmfn  22701  pjnmopi  22744  orvcval2  23674  derangenlem  23717  dfrtrcl2  24060  dfon2lem3  24212  dfon2lem7  24216  fnimage  24539  imageval  24540  supadd  24996  itg2addnc  25005  elo  25144  valcurfn  25306  intopcoaconlem3b  25641  intopcoaconlem3  25642  qusp  25645  dfiunv2  26019  cndpv  26152  pgapspf  26155  bhp2a  26279  sdclem2  26555  sdclem1  26556  heibor1lem  26636  eldiophss  26957  setindtrs  27221  hbtlem2  27431  hbtlem5  27435  rngunsnply  27481  psgnvali  27534  glbconxN  30189  pmapglbx  30580  dvhb1dimN  31797
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator