Theorem rabex 5333

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)

Hypothesis

Ref	Expression
rabex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
rabex	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabex

Step	Hyp	Ref	Expression
1		rabex.1	. 2 ⊢ 𝐴 ∈ V
2		rabexg 5332	. 2 ⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Syntax hints:   ∈ wcel 2107  {crab 3433  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  rab2ex  5336  frminex  5657  ssimaex  6977  fvmptrabfv  7030  mptrabex  7227  fnpm  8828  inf3lema  9619  dfac2a  10124  kmlem1  10145  axcc4  10434  axdc3lem2  10446  axdc3lem4  10448  pwfseqlem1  10653  dfuzi  12653  uzval  12824  ixxval  13332  fzval  13486  bitsfval  16364  sadfval  16393  smufval  16418  phicl2  16701  hashgcdeq  16722  prmreclem4  16852  prmreclem5  16853  ismre  17534  fnmre  17535  mrisval  17574  isacs  17595  ismon  17680  isnat  17898  natffn  17900  initofn  17937  termofn  17938  initoval  17943  termoval  17944  coafval  18014  ismhm  18673  issubm  18684  issubg  19006  isnsg  19035  gimfn  19135  isgim  19136  isga  19155  cntzval  19185  odfval  19400  odngen  19445  gexval  19446  isslw  19476  ablfac1a  19939  ablfac1b  19940  ablfac1c  19941  ablfac1eu  19943  ablfaclem1  19955  ablfaclem2  19956  ablfaclem3  19957  isirred  20233  isrim0OLD  20259  isrim0  20261  issubrg  20319  issdrg  20404  abvfval  20426  lssset  20544  lmimfn  20637  islmhm  20638  islmim  20673  islbs  20687  rrgval  20903  ocvval  21220  elocv  21221  isobs  21275  islinds  21364  psrval  21468  psraddcl  21502  psrvscacl  21512  psrgrp  21517  psrgrpOLD  21518  psrlmod  21521  subrgpsr  21539  mvrf  21544  mplsubrg  21564  mplmonmul  21591  mplbas2  21597  opsrval  21601  mhpval  21683  mhpmulcl  21692  mhpinvcl  21695  psrplusgpropd  21758  psropprmul  21760  scmatval  22006  fncld  22526  cnfval  22737  cnpval  22740  iscnp2  22743  1stcfb  22949  kgenf  23045  xkoopn  23093  dfac14  23122  hmeofn  23261  hmeofval  23262  filunirn  23386  alexsubALTlem2  23552  ucnval  23782  iscfilu  23793  ispsmet  23810  ismet  23829  isxmet  23830  xmetunirn  23843  cncfval  24404  ishtpy  24488  isphtpy  24497  om1bas  24547  cfilfval  24781  caufval  24792  iscmet  24801  dyadmax  25115  vitalilem2  25126  vitalilem3  25127  vitalilem4  25128  itg2monolem1  25268  fncpn  25450  elcpn  25451  mdeg0  25588  mdegaddle  25592  mdegvsca  25594  uc1pval  25657  mon1pval  25659  aannenlem1  25841  aannenlem2  25842  aannenlem3  25843  vmaval  26617  sqff1o  26686  musum  26695  dchrval  26737  dchrbas  26738  leftval  27358  rightval  27359  leftf  27360  rightf  27361  precsexlem4  27656  precsexlem5  27657  tglnfn  27798  tglnunirn  27799  tglngval  27802  israg  27948  iseqlg  28118  ttgitvval  28139  ebtwntg  28240  incistruhgr  28339  usgredgleordALT  28491  vtxdun  28738  vtxdlfgrval  28742  vtxd0nedgb  28745  vtxdushgrfvedglem  28746  vtxdushgrfvedg  28747  vtxdusgr0edgnelALT  28753  1loopgrvd2  28760  usgrvd0nedg  28790  rusgrnumwrdl2  28843  ewlksfval  28858  wwlksn  29091  wspthsn  29102  iswwlksnon  29107  iswspthsnon  29110  wlknwwlksnen  29143  wwlksnexthasheq  29157  rusgrnumwlkg  29231  clwlkclwwlken  29265  clwwlkn  29279  clwwlken  29305  clwlkssizeeq  29338  clwwlknon  29343  clwwlk0on0  29345  konigsberglem5  29509  fusgreg2wsplem  29586  fusgreghash2wsp  29591  2clwwlk  29600  clwwlknonclwlknonen  29616  numclwlk1lem2  29623  numclwwlkovh0  29625  numclwwlkovq  29627  numclwwlkqhash  29628  lnoval  30005  bloval  30034  hmoval  30063  ubthlem1  30123  ubthlem2  30124  ocval  30533  eigvecval  31149  specval  31151  rabfodom  31743  fpwrelmap  31958  nsgmgc  32523  mxidlval  32577  ssmxidl  32590  rprmval  32633  locfinreflem  32820  rspectopn  32847  zarcls1  32849  zarclsun  32850  zarclsiin  32851  zarclsint  32852  zarclssn  32853  zarcls  32854  zartopn  32855  zar0ring  32858  zart0  32859  zarmxt1  32860  zarcmplem  32861  rhmpreimacnlem  32864  rhmpreimacn  32865  ordtconnlem1  32904  sigaex  33108  ddemeas  33234  ismbfm  33249  elunirnmbfm  33250  eulerpart  33381  ballotlem8  33535  reprval  33622  bnj110  33869  fncvm  34248  iscvm  34250  snmlval  34322  satfv1  34354  satfdm  34360  satffunlem1lem2  34394  satfv0fvfmla0  34404  satfv1fvfmla1  34414  mpstval  34526  fvray  35113  icoreval  36234  fin2solem  36474  fin2so  36475  poimirlem4  36492  cnambfre  36536  istotbnd  36637  isbnd  36648  rngohomval  36832  rngoisoval  36845  idlval  36881  pridlval  36901  maxidlval  36907  lshpset  37848  lflset  37929  pats  38155  llnset  38376  lplnset  38400  lvolset  38443  isline  38610  pmapval  38628  paddval  38669  lhpset  38866  ldilset  38980  ltrnset  38989  dilsetN  39024  trnsetN  39027  diaval  39903  diafn  39905  lpolsetN  40353  lcdvadd  40468  lcdsca  40470  lcdvs  40474  mapdval  40499  mapd1o  40519  mhmcompl  41120  mhmcoaddmpl  41123  rhmcomulmpl  41124  evlselv  41159  mhphf  41169  prjcrvval  41374  isnacs  41442  mzpclval  41463  pell1qrval  41584  pell14qrval  41586  pell1234qrval  41588  elmnc  41878  itgoval  41903  idomodle  41938  idomsubgmo  41940  k0004val  42901  icof  43918  elicores  44246  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  stoweidlem34  44750  fourierdlem2  44825  fourierdlem3  44826  etransclem12  44962  etransclem33  44983  ovnval2b  45268  volicorescl  45269  ovncvrrp  45280  ovnsubaddlem1  45286  ovncvr2  45327  issmflem  45443  smfaddlem1  45479  smfaddlem2  45480  smflimlem1  45487  fvmptrabdm  46001  iccpval  46083  fppr  46394  ismgmhm  46553  issubmgm  46559  assintopval  46615  rnghmfn  46688  rnghmval  46689  isrngisom  46694  issubrng  46726  rngchomrnghmresALTV  46894  bigoval  47235  elbigofrcl  47236  line  47418  rrxline  47420  sphere  47433  rrxsphere  47434