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

Theorem rabex 4357
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
rabex.1  |-  A  e. 
_V
Assertion
Ref Expression
rabex  |-  { x  e.  A  |  ph }  e.  _V
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rabex
StepHypRef Expression
1 rabex.1 . 2  |-  A  e. 
_V
2 rabexg 4356 . 2  |-  ( A  e.  _V  ->  { x  e.  A  |  ph }  e.  _V )
31, 2ax-mp 5 1  |-  { x  e.  A  |  ph }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   {crab 2711   _Vcvv 2958
This theorem is referenced by:  frminex  4565  ssimaex  5791  fnpm  7029  inf3lema  7582  cantnffval  7621  dfac2a  8015  kmlem1  8035  axcc4  8324  axdc3lem2  8336  axdc3lem4  8338  pwfseqlem1  8538  nqex  8805  dfuzi  10365  uzval  10495  ixxval  10929  fzval  11050  bitsfval  12940  sadfval  12969  smufval  12994  phicl2  13162  odzval  13182  prmreclem4  13292  prmreclem5  13293  ismre  13820  fnmre  13821  mrisval  13860  isacs  13881  ismon  13964  isnat  14149  natffn  14151  coafval  14224  ismhm  14745  issubm  14753  gsumvalx  14779  issubg  14949  isnsg  14974  gimfn  15053  isgim  15054  isga  15073  cntzval  15125  odval  15177  odf  15180  odngen  15216  gexval  15217  sylow1lem2  15238  isslw  15247  sylow3lem6  15271  dmdprd  15564  dprdval  15566  ablfac1a  15632  ablfac1b  15633  ablfac1c  15634  ablfac1eu  15636  ablfaclem1  15648  ablfaclem2  15649  ablfaclem3  15650  isirred  15809  issubrg  15873  abvfval  15911  lssset  16015  lmimfn  16107  islmhm  16108  islmim  16139  islbs  16153  rrgval  16352  psrval  16434  gsumbagdiag  16446  psrbas  16448  psrelbas  16449  psraddcl  16452  psrmulfval  16454  psrmulcllem  16456  psrvscaval  16461  psrvscacl  16462  psr0cl  16463  psr0lid  16464  psrnegcl  16465  psrlinv  16466  psrgrp  16467  psrlmod  16470  psr1cl  16471  psrlidm  16472  psrridm  16473  psrdi  16475  psrdir  16476  psrass23  16478  subrgpsr  16487  mvrval  16490  mvrf  16493  mplsubglem  16503  mplvscaval  16516  mplmon  16531  mplcoe1  16533  mplbas2  16536  ltbval  16537  opsrval  16540  opsrtoslem2  16550  mplmon2  16558  evlslem2  16573  psrplusgpropd  16634  psropprmul  16637  ocvval  16899  elocv  16900  isobs  16952  fncld  17091  cnfval  17302  cnpval  17305  iscnp2  17308  1stcfb  17513  kgenf  17578  xkoopn  17626  dfac14  17655  hmeofn  17794  hmeofval  17795  filunirn  17919  alexsubALTlem2  18084  ucnval  18312  iscfilu  18323  ispsmet  18340  ismet  18358  isxmet  18359  xmetunirn  18372  cncfval  18923  ishtpy  19002  isphtpy  19011  om1bas  19061  cfilfval  19222  caufval  19233  iscmet  19242  dyadmax  19495  vitalilem2  19506  vitalilem3  19507  vitalilem4  19508  itg2monolem1  19645  fncpn  19824  elcpn  19825  evlslem3  19940  evlslem1  19941  mdegaddle  20002  mdegvsca  20004  mdegmullem  20006  uc1pval  20067  mon1pval  20069  aannenlem1  20250  aannenlem2  20251  aannenlem3  20252  vmaval  20901  vmaf  20907  sqff1o  20970  musum  20981  0sgmppw  20987  dchrval  21023  dchrbas  21024  lnoval  22258  bloval  22287  hmoval  22316  ubthlem1  22377  ubthlem2  22378  ocval  22787  eigvecval  23404  specval  23406  sigaex  24497  isrnsigaOLD  24500  ismbfm  24607  elunirnmbfm  24608  sitgval  24652  ballotlem8  24799  lgamgulmlem5  24822  lgamgulmlem6  24823  lgamgulm2  24825  lgamcvglem  24829  fncvm  24949  iscvm  24951  snmlval  25023  elgiso  25112  fvray  26080  cnambfre  26267  istotbnd  26492  isbnd  26503  rngohomval  26594  rngoisoval  26607  idlval  26637  pridlval  26657  maxidlval  26663  isnacs  26772  mzpclval  26796  pell1qrval  26923  pell14qrval  26925  pell1234qrval  26927  mapfien2  27249  pwfi2en  27252  islinds  27270  elmnc  27332  itgoval  27357  pmtrfval  27384  psgnfval  27414  issdrg  27496  idomodle  27503  idomsubgmo  27505  hashgcdeq  27508  stoweidlem34  27773  bnj110  29303  lshpset  29850  lflset  29931  pats  30157  llnset  30376  lplnset  30400  lvolset  30443  isline  30610  pmapval  30628  paddval  30669  lhpset  30866  ldilset  30980  ltrnset  30989  dilsetN  31024  trnsetN  31027  diafval  31903  diaval  31904  diafn  31906  dicfval  32047  lpolsetN  32354  lcdvadd  32469  lcdsca  32471  lcdvs  32475  mapdval  32500  mapd1o  32520  mapdunirnN  32522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator