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

Theorem elab 2865
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 2864 1  |-  ( A  e.  { x  | 
ph }  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1619    e. wcel 1621   {cab 2242   _Vcvv 2740
This theorem is referenced by:  ralab  2877  rexab  2879  intab  3833  dfiin2g  3877  uniuni  4464  finds  4619  finds2  4621  opeliunxp  4693  funcnvuni  5220  fun11iun  5396  elabrex  5664  abrexco  5665  tfrlem3  6326  mapval2  6730  sbthlem2  6905  ssenen  6968  dffi2  7109  dffi3  7117  tctr  7358  tcmin  7359  tc2  7360  tz9.13  7396  tcrank  7487  kardex  7497  karden  7498  cardf2  7509  cardiun  7548  alephval3  7670  dfac3  7681  dfac5lem3  7685  dfac5lem4  7686  dfac2  7690  kmlem12  7720  cardcf  7811  cfeq0  7815  cfsuc  7816  cff1  7817  cflim2  7822  cfss  7824  axdc3lem2  8010  axdc3lem3  8011  axdclem  8079  brdom7disj  8089  brdom6disj  8090  tskuni  8338  gruina  8373  nqpr  8571  supmul  9655  dfnn2  9692  dfuzi  10034  seqof  11034  hashfacen  11322  hashf1lem1  11323  hashf1lem2  11324  shftfval  11495  infcvgaux1i  12242  efgrelexlemb  14986  lss1d  15647  lidldvgen  15934  zndvds  16430  cmpsublem  17053  cmpsub  17054  ptpjopn  17233  ptclsg  17236  txdis1cn  17256  tx1stc  17271  hauspwpwf1  17609  divstgplem  17730  i1fadd  18977  i1fmul  18978  i1fmulc  18985  mpfind  19355  pf1ind  19365  nmosetn0  21268  nmoolb  21274  nmlno0lem  21296  nmopsetn0  22370  nmfnsetn0  22383  nmoplb  22412  nmfnlb  22429  nmlnop0iALT  22500  nmopun  22519  nmcexi  22531  branmfn  22610  pjnmopi  22653  derangenlem  23039  dfrtrcl2  23382  dfon2lem3  23475  dfon2lem7  23479  fnimage  23808  imageval  23809  elo  24372  valcurfn  24535  intopcoaconlem3b  24870  intopcoaconlem3  24871  qusp  24874  dfiunv2  25248  cndpv  25381  pgapspf  25384  bhp2a  25508  sdclem2  25784  sdclem1  25785  heibor1lem  25865  eldiophss  26186  setindtrs  26450  hbtlem2  26660  hbtlem5  26664  rngunsnply  26710  psgnvali  26763  glbconxN  28697  pmapglbx  29088  dvhb1dimN  30305
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742
  Copyright terms: Public domain W3C validator