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

Theorem elab 3074
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 3073 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {cab 2421   _Vcvv 2948
This theorem is referenced by:  ralab  3087  rexab  3089  intab  4072  dfiin2g  4116  dfiunv2  4119  uniuni  4708  finds  4863  finds2  4865  opeliunxp  4921  funcnvuni  5510  fun11iun  5687  elabrex  5977  abrexco  5978  tfrlem3  6630  mapval2  7035  sbthlem2  7210  ssenen  7273  dffi2  7420  dffi3  7428  tctr  7671  tcmin  7672  tc2  7673  tz9.13  7709  tcrank  7800  kardex  7810  karden  7811  cardf2  7822  cardiun  7861  alephval3  7983  dfac3  7994  dfac5lem3  7998  dfac5lem4  7999  dfac2  8003  kmlem12  8033  cardcf  8124  cfeq0  8128  cfsuc  8129  cff1  8130  cflim2  8135  cfss  8137  axdc3lem2  8323  axdc3lem3  8324  axdclem  8391  brdom7disj  8401  brdom6disj  8402  tskuni  8650  gruina  8685  nqpr  8883  supmul  9968  dfnn2  10005  dfuzi  10352  seqof  11372  hashfacen  11695  hashf1lem1  11696  hashf1lem2  11697  shftfval  11877  infcvgaux1i  12628  efgrelexlemb  15374  lss1d  16031  lidldvgen  16318  zndvds  16822  cmpsublem  17454  cmpsub  17455  ptpjopn  17636  ptclsg  17639  txdis1cn  17659  tx1stc  17674  hauspwpwf1  18011  divstgplem  18142  ustn0  18242  i1fadd  19579  i1fmul  19580  i1fmulc  19587  mpfind  19957  pf1ind  19967  nmosetn0  22258  nmoolb  22264  nmlno0lem  22286  nmopsetn0  23360  nmfnsetn0  23373  nmoplb  23402  nmfnlb  23419  nmlnop0iALT  23490  nmopun  23509  nmcexi  23521  branmfn  23600  pjnmopi  23643  esumc  24438  orvcval2  24708  derangenlem  24849  dfrtrcl2  25140  dfon2lem3  25404  dfon2lem7  25408  fnimage  25766  imageval  25767  supadd  26229  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  itg2addnc  26249  sdclem2  26437  sdclem1  26438  heibor1lem  26509  eldiophss  26824  setindtrs  27087  hbtlem2  27296  hbtlem5  27300  rngunsnply  27346  psgnvali  27399  2wot2wont  28306  2spot2iun2spont  28311  usg2spot2nb  28391  glbconxN  30112  pmapglbx  30503  dvhb1dimN  31720
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950
  Copyright terms: Public domain W3C validator