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

Theorem elab 2916
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 1607 . 2  |-  F/ x ps
2 elab.1 . 2  |-  A  e. 
_V
3 elab.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3elabf 2915 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1625    e. wcel 1686   {cab 2271   _Vcvv 2790
This theorem is referenced by:  ralab  2928  rexab  2930  intab  3894  dfiin2g  3938  uniuni  4529  finds  4684  finds2  4686  opeliunxp  4742  funcnvuni  5319  fun11iun  5495  elabrex  5767  abrexco  5768  tfrlem3  6395  mapval2  6799  sbthlem2  6974  ssenen  7037  dffi2  7178  dffi3  7186  tctr  7427  tcmin  7428  tc2  7429  tz9.13  7465  tcrank  7556  kardex  7566  karden  7567  cardf2  7578  cardiun  7617  alephval3  7739  dfac3  7750  dfac5lem3  7754  dfac5lem4  7755  dfac2  7759  kmlem12  7789  cardcf  7880  cfeq0  7884  cfsuc  7885  cff1  7886  cflim2  7891  cfss  7893  axdc3lem2  8079  axdc3lem3  8080  axdclem  8148  brdom7disj  8158  brdom6disj  8159  tskuni  8407  gruina  8442  nqpr  8640  supmul  9724  dfnn2  9761  dfuzi  10104  seqof  11105  hashfacen  11394  hashf1lem1  11395  hashf1lem2  11396  shftfval  11567  infcvgaux1i  12317  efgrelexlemb  15061  lss1d  15722  lidldvgen  16009  zndvds  16505  cmpsublem  17128  cmpsub  17129  ptpjopn  17308  ptclsg  17311  txdis1cn  17331  tx1stc  17346  hauspwpwf1  17684  divstgplem  17805  i1fadd  19052  i1fmul  19053  i1fmulc  19060  mpfind  19430  pf1ind  19440  nmosetn0  21345  nmoolb  21351  nmlno0lem  21373  nmopsetn0  22447  nmfnsetn0  22460  nmoplb  22489  nmfnlb  22506  nmlnop0iALT  22577  nmopun  22596  nmcexi  22608  branmfn  22687  pjnmopi  22730  orvcval2  23661  derangenlem  23704  dfrtrcl2  24047  dfon2lem3  24143  dfon2lem7  24147  fnimage  24470  imageval  24471  supadd  24928  itg2addnc  24935  elo  25052  valcurfn  25214  intopcoaconlem3b  25549  intopcoaconlem3  25550  qusp  25553  dfiunv2  25927  cndpv  26060  pgapspf  26063  bhp2a  26187  sdclem2  26463  sdclem1  26464  heibor1lem  26544  eldiophss  26865  setindtrs  27129  hbtlem2  27339  hbtlem5  27343  rngunsnply  27389  psgnvali  27442  glbconxN  29640  pmapglbx  30031  dvhb1dimN  31248
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792
  Copyright terms: Public domain W3C validator