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

Theorem rabex 4550
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 4549 . 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 setvar class
Syntax hints:    e. wcel 1904   {crab 2760   _Vcvv 3031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-in 3397  df-ss 3404
This theorem is referenced by:  rab2ex  4553  rab2exOLD  4555  frminex  4819  ssimaex  5945  mptrabex  6153  mptrabexOLD  6154  fnpm  7498  inf3lema  8147  dfac2a  8578  kmlem1  8598  axcc4  8887  axdc3lem2  8899  axdc3lem4  8901  pwfseqlem1  9101  dfuzi  11049  uzval  11184  ixxval  11668  fzval  11812  bitsfval  14475  sadfval  14505  smufval  14530  phicl2  14795  prmreclem4  14942  prmreclem5  14943  ismre  15574  fnmre  15575  mrisval  15614  isacs  15635  ismon  15716  isnat  15930  natffn  15932  initoval  15970  termoval  15971  coafval  16037  ismhm  16662  issubm  16672  issubg  16895  isnsg  16924  gimfn  17003  isgim  17004  isga  17023  cntzval  17053  odngen  17304  gexval  17305  gexvalOLD  17307  isslw  17338  ablfac1a  17780  ablfac1b  17781  ablfac1c  17782  ablfac1eu  17784  ablfaclem1  17796  ablfaclem2  17797  ablfaclem3  17798  isirred  18005  isrim0  18029  issubrg  18086  abvfval  18124  lssset  18235  lmimfn  18327  islmhm  18328  islmim  18363  islbs  18377  rrgval  18588  psrval  18663  psraddcl  18684  psrvscacl  18694  psrgrp  18699  psrlmod  18702  subrgpsr  18720  mvrf  18725  mplsubrg  18741  mplmonmul  18765  mplbas2  18771  opsrval  18775  psrplusgpropd  18906  psropprmul  18908  ocvval  19307  elocv  19308  isobs  19360  islinds  19444  scmatval  19606  fncld  20114  cnfval  20326  cnpval  20329  iscnp2  20332  1stcfb  20537  kgenf  20633  xkoopn  20681  dfac14  20710  hmeofn  20849  hmeofval  20850  filunirn  20975  alexsubALTlem2  21141  ucnval  21370  iscfilu  21381  ispsmet  21398  ismet  21416  isxmet  21417  xmetunirn  21430  cncfval  21998  ishtpy  22081  isphtpy  22090  om1bas  22140  cfilfval  22312  caufval  22323  iscmet  22332  dyadmax  22635  vitalilem2  22646  vitalilem3  22647  vitalilem4  22648  itg2monolem1  22787  fncpn  22966  elcpn  22967  mdegleb  23092  mdeg0  23098  mdegaddle  23102  mdegvsca  23104  uc1pval  23169  mon1pval  23171  aannenlem1  23363  aannenlem2  23364  aannenlem3  23365  vmaval  24119  sqff1o  24188  musum  24199  0sgmppw  24205  dchrval  24241  dchrbas  24242  tglnfn  24671  tglnunirn  24672  tglngval  24675  israg  24821  iseqlg  24976  ttgitvval  24991  ebtwntg  25091  clwlksizeeq  25659  rusgranumwlklem1  25756  rusgranumwlklem3  25758  rusgranumwlklem4  25759  rusgranumwwlkg  25766  numclwwlkovf  25888  numclwwlkovg  25894  numclwwlkovq  25906  numclwwlkqhash  25907  numclwwlkovh  25908  lnoval  26474  bloval  26503  hmoval  26532  ubthlem1  26593  ubthlem2  26594  ocval  27014  eigvecval  27630  specval  27632  rabfodom  28219  fpwrelmap  28393  locfinreflem  28741  ordtconlem1  28804  sigaex  29005  isrnsigaOLD  29008  ddemeas  29132  ismbfm  29147  elunirnmbfm  29148  eulerpart  29288  ballotlem8  29442  ballotlem8OLD  29480  bnj110  29741  fncvm  30052  iscvm  30054  snmlval  30126  mpstval  30245  elgiso  30386  fvray  30979  icoreval  31826  fin2solem  31995  fin2so  31996  poimirlem4  32008  cnambfre  32053  istotbnd  32165  isbnd  32176  rngohomval  32267  rngoisoval  32280  idlval  32310  pridlval  32330  maxidlval  32336  lshpset  32615  lflset  32696  pats  32922  llnset  33141  lplnset  33165  lvolset  33208  isline  33375  pmapval  33393  paddval  33434  lhpset  33631  ldilset  33745  ltrnset  33754  dilsetN  33790  trnsetN  33793  diaval  34671  diafn  34673  lpolsetN  35121  lcdvadd  35236  lcdsca  35238  lcdvs  35242  mapdval  35267  mapd1o  35287  isnacs  35617  mzpclval  35638  pell1qrval  35763  pell14qrval  35765  pell1234qrval  35767  elmnc  36066  itgoval  36098  issdrg  36134  idomodle  36141  idomsubgmo  36143  hashgcdeq  36146  icof  37572  elicores  37731  dvnprodlem1  37918  dvnprodlem2  37919  dvnprodlem3  37920  stoweidlem34  38007  fourierdlem2  38083  fourierdlem3  38084  etransclem12  38223  etransclem33  38244  ovnval2b  38492  volicorescl  38493  ovncvrrp  38504  ovnsubaddlem1  38510  ovncvr2  38551  iccpval  38874  incistruhgr  39325  usgredgaleordALT  39475  nbedgusgr  39610  uvtxaval  39623  vtxdun  39704  vtxdlfgrval  39708  vtxd0nedgb  39711  vtxdushgrfvedglem  39712  vtxdushgrfvedg  39713  vtxdusgr0edgnelALT  39719  1loopgrvd2  39725  hashnbusgrvd  39751  usgrvd0nedg  39756  ewlksfval  39807  konigsberglem5  40170  usgsizedg  40215  usgsizedgALT  40216  usgsizedgALT2  40217  fiusgedgfi  40252  fiusgedgfiALT  40253  ismgmhm  40291  issubmgm  40297  assintopval  40349  rnghmfn  40398  rnghmval  40399  isrngisom  40404  rngchomrnghmresALTV  40506  bigoval  40868  elbigofrcl  40869
  Copyright terms: Public domain W3C validator