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

Theorem elab 2851
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 2850 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2239   _Vcvv 2727
This theorem is referenced by:  ralab  2863  rexab  2865  intab  3790  dfiin2g  3834  uniuni  4418  finds  4573  finds2  4575  opeliunxp  4647  funcnvuni  5174  fun11iun  5350  elabrex  5617  abrexco  5618  tfrlem3  6279  mapval2  6683  sbthlem2  6857  ssenen  6920  dffi2  7060  dffi3  7068  tctr  7309  tcmin  7310  tc2  7311  tz9.13  7347  tcrank  7438  kardex  7448  karden  7449  cardf2  7460  cardiun  7499  alephval3  7621  dfac3  7632  dfac5lem3  7636  dfac5lem4  7637  dfac2  7641  kmlem12  7671  cardcf  7762  cfeq0  7766  cfsuc  7767  cff1  7768  cflim2  7773  cfss  7775  axdc3lem2  7961  axdc3lem3  7962  axdclem  8030  brdom7disj  8040  brdom6disj  8041  tskuni  8285  gruina  8320  nqpr  8518  supmul  9602  dfnn2  9639  dfuzi  9981  seqof  10981  hashfacen  11269  hashf1lem1  11270  hashf1lem2  11271  shftfval  11442  infcvgaux1i  12189  efgrelexlemb  14894  lss1d  15555  lidldvgen  15839  zndvds  16335  cmpsublem  16958  cmpsub  16959  ptpjopn  17138  ptclsg  17141  txdis1cn  17161  tx1stc  17176  hauspwpwf1  17514  divstgplem  17635  i1fadd  18882  i1fmul  18883  i1fmulc  18890  mpfind  19260  pf1ind  19270  nmosetn0  21173  nmoolb  21179  nmlno0lem  21201  nmopsetn0  22275  nmfnsetn0  22288  nmoplb  22317  nmfnlb  22334  nmlnop0iALT  22405  nmopun  22424  nmcexi  22436  branmfn  22515  pjnmopi  22558  derangenlem  22873  dfrtrcl2  23216  dfon2lem3  23309  dfon2lem7  23313  fnimage  23642  imageval  23643  elo  24206  valcurfn  24369  intopcoaconlem3b  24704  intopcoaconlem3  24705  qusp  24708  dfiunv2  25082  cndpv  25215  pgapspf  25218  bhp2a  25342  sdclem2  25618  sdclem1  25619  heibor1lem  25699  eldiophss  26020  setindtrs  26284  hbtlem2  26494  hbtlem5  26498  rngunsnply  26544  psgnvali  26597  glbconxN  28256  pmapglbx  28647  dvhb1dimN  29864
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729
  Copyright terms: Public domain W3C validator