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

Theorem elab 3046
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 1626 . 2  |-  F/ x ps
2 elab.1 . 2  |-  A  e. 
_V
3 elab.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabf 3045 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721   {cab 2394   _Vcvv 2920
This theorem is referenced by:  ralab  3059  rexab  3061  intab  4044  dfiin2g  4088  dfiunv2  4091  uniuni  4679  finds  4834  finds2  4836  opeliunxp  4892  funcnvuni  5481  fun11iun  5658  elabrex  5948  abrexco  5949  tfrlem3  6601  mapval2  7006  sbthlem2  7181  ssenen  7244  dffi2  7390  dffi3  7398  tctr  7639  tcmin  7640  tc2  7641  tz9.13  7677  tcrank  7768  kardex  7778  karden  7779  cardf2  7790  cardiun  7829  alephval3  7951  dfac3  7962  dfac5lem3  7966  dfac5lem4  7967  dfac2  7971  kmlem12  8001  cardcf  8092  cfeq0  8096  cfsuc  8097  cff1  8098  cflim2  8103  cfss  8105  axdc3lem2  8291  axdc3lem3  8292  axdclem  8359  brdom7disj  8369  brdom6disj  8370  tskuni  8618  gruina  8653  nqpr  8851  supmul  9936  dfnn2  9973  dfuzi  10320  seqof  11339  hashfacen  11662  hashf1lem1  11663  hashf1lem2  11664  shftfval  11844  infcvgaux1i  12595  efgrelexlemb  15341  lss1d  15998  lidldvgen  16285  zndvds  16789  cmpsublem  17420  cmpsub  17421  ptpjopn  17601  ptclsg  17604  txdis1cn  17624  tx1stc  17639  hauspwpwf1  17976  divstgplem  18107  ustn0  18207  i1fadd  19544  i1fmul  19545  i1fmulc  19552  mpfind  19922  pf1ind  19932  nmosetn0  22223  nmoolb  22229  nmlno0lem  22251  nmopsetn0  23325  nmfnsetn0  23338  nmoplb  23367  nmfnlb  23384  nmlnop0iALT  23455  nmopun  23474  nmcexi  23486  branmfn  23565  pjnmopi  23608  esumc  24403  orvcval2  24673  derangenlem  24814  dfrtrcl2  25105  dfon2lem3  25359  dfon2lem7  25363  fnimage  25686  imageval  25687  supadd  26142  mblfinlem2  26148  mblfinlem3  26149  ismblfin  26150  itg2addnc  26162  sdclem2  26340  sdclem1  26341  heibor1lem  26412  eldiophss  26727  setindtrs  26990  hbtlem2  27200  hbtlem5  27204  rngunsnply  27250  psgnvali  27303  2wot2wont  28087  2spot2iun2spont  28092  usg2spot2nb  28172  glbconxN  29864  pmapglbx  30255  dvhb1dimN  31472
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922
  Copyright terms: Public domain W3C validator