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

Theorem elab 2889
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 2888 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2244   _Vcvv 2763
This theorem is referenced by:  ralab  2901  rexab  2903  intab  3866  dfiin2g  3910  uniuni  4499  finds  4654  finds2  4656  opeliunxp  4728  funcnvuni  5255  fun11iun  5431  elabrex  5699  abrexco  5700  tfrlem3  6361  mapval2  6765  sbthlem2  6940  ssenen  7003  dffi2  7144  dffi3  7152  tctr  7393  tcmin  7394  tc2  7395  tz9.13  7431  tcrank  7522  kardex  7532  karden  7533  cardf2  7544  cardiun  7583  alephval3  7705  dfac3  7716  dfac5lem3  7720  dfac5lem4  7721  dfac2  7725  kmlem12  7755  cardcf  7846  cfeq0  7850  cfsuc  7851  cff1  7852  cflim2  7857  cfss  7859  axdc3lem2  8045  axdc3lem3  8046  axdclem  8114  brdom7disj  8124  brdom6disj  8125  tskuni  8373  gruina  8408  nqpr  8606  supmul  9690  dfnn2  9727  dfuzi  10070  seqof  11070  hashfacen  11358  hashf1lem1  11359  hashf1lem2  11360  shftfval  11531  infcvgaux1i  12278  efgrelexlemb  15022  lss1d  15683  lidldvgen  15970  zndvds  16466  cmpsublem  17089  cmpsub  17090  ptpjopn  17269  ptclsg  17272  txdis1cn  17292  tx1stc  17307  hauspwpwf1  17645  divstgplem  17766  i1fadd  19013  i1fmul  19014  i1fmulc  19021  mpfind  19391  pf1ind  19401  nmosetn0  21304  nmoolb  21310  nmlno0lem  21332  nmopsetn0  22406  nmfnsetn0  22419  nmoplb  22448  nmfnlb  22465  nmlnop0iALT  22536  nmopun  22555  nmcexi  22567  branmfn  22646  pjnmopi  22689  derangenlem  23075  dfrtrcl2  23418  dfon2lem3  23511  dfon2lem7  23515  fnimage  23844  imageval  23845  elo  24408  valcurfn  24571  intopcoaconlem3b  24906  intopcoaconlem3  24907  qusp  24910  dfiunv2  25284  cndpv  25417  pgapspf  25420  bhp2a  25544  sdclem2  25820  sdclem1  25821  heibor1lem  25901  eldiophss  26222  setindtrs  26486  hbtlem2  26696  hbtlem5  26700  rngunsnply  26746  psgnvali  26799  glbconxN  28817  pmapglbx  29208  dvhb1dimN  30425
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765
  Copyright terms: Public domain W3C validator