Theorem rabex 5309

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 5307	. 2 ⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V

Syntax hints:   ∈ wcel 2108  {crab 3415  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  rab2ex  5312  frminex  5633  ssimaex  6963  fvmptrabfv  7017  mptrabex  7216  fnpm  8846  inf3lema  9636  dfac2a  10142  kmlem1  10163  axcc4  10451  axdc3lem2  10463  axdc3lem4  10465  pwfseqlem1  10670  dfuzi  12682  uzval  12852  ixxval  13368  fzval  13524  bitsfval  16440  sadfval  16469  smufval  16494  phicl2  16785  hashgcdeq  16807  prmreclem4  16937  prmreclem5  16938  ismre  17600  fnmre  17601  mrisval  17640  isacs  17661  ismon  17744  isnat  17961  natffn  17963  initofn  17998  termofn  17999  initoval  18004  termoval  18005  coafval  18075  ismgmhm  18672  issubmgm  18678  ismhm  18761  issubm  18779  issubg  19107  isnsg  19136  gimfn  19242  isgim  19243  isga  19272  cntzval  19302  odfval  19511  odngen  19556  gexval  19557  isslw  19587  ablfac1a  20050  ablfac1b  20051  ablfac1c  20052  ablfac1eu  20054  ablfaclem1  20066  ablfaclem2  20067  ablfaclem3  20068  isirred  20377  rnghmfn  20397  rnghmval  20398  isrngim  20403  isrim0OLD  20439  isrim0  20441  issubrng  20505  issubrg  20529  rrgval  20655  issdrg  20746  abvfval  20768  lssset  20888  lmimfn  20982  islmhm  20983  islmim  21018  islbs  21032  ocvval  21625  elocv  21626  isobs  21678  islinds  21767  psrval  21873  psraddcl  21896  psraddclOLD  21897  psrvscacl  21909  psrgrp  21914  psrgrpOLD  21915  psrlmod  21918  subrgpsr  21936  mvrf  21943  mplsubrg  21963  mplmonmul  21992  mplbas2  21998  opsrval  22002  mhpval  22075  mhpmulcl  22085  mhpinvcl  22088  psdcl  22097  psdmplcl  22098  psdadd  22099  psdmul  22102  psrplusgpropd  22169  psropprmul  22171  rhmcomulmpl  22318  scmatval  22440  fncld  22958  cnfval  23169  cnpval  23172  iscnp2  23175  1stcfb  23381  kgenf  23477  xkoopn  23525  dfac14  23554  hmeofn  23693  hmeofval  23694  filunirn  23818  alexsubALTlem2  23984  ucnval  24213  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  xmetunirn  24274  cncfval  24830  ishtpy  24920  isphtpy  24929  om1bas  24980  cfilfval  25214  caufval  25225  iscmet  25234  dyadmax  25549  vitalilem2  25560  vitalilem3  25561  vitalilem4  25562  itg2monolem1  25701  fncpn  25885  elcpn  25886  mdeg0  26025  mdegaddle  26029  mdegvsca  26031  uc1pval  26095  mon1pval  26097  aannenlem1  26286  aannenlem2  26287  aannenlem3  26288  vmaval  27073  sqff1o  27142  musum  27151  dchrval  27195  dchrbas  27196  leftval  27819  rightval  27820  leftf  27821  rightf  27822  precsexlem4  28151  precsexlem5  28152  tglnfn  28472  tglnunirn  28473  tglngval  28476  israg  28622  iseqlg  28792  ttgitvval  28807  ebtwntg  28907  incistruhgr  29004  usgredgleordALT  29159  vtxdun  29407  vtxdlfgrval  29411  vtxd0nedgb  29414  vtxdushgrfvedglem  29415  vtxdushgrfvedg  29416  vtxdusgr0edgnelALT  29422  1loopgrvd2  29429  usgrvd0nedg  29459  rusgrnumwrdl2  29512  ewlksfval  29527  wwlksn  29765  wspthsn  29776  iswwlksnon  29781  iswspthsnon  29784  wlknwwlksnen  29817  wwlksnexthasheq  29831  rusgrnumwlkg  29905  clwlkclwwlken  29939  clwwlkn  29953  clwwlken  29979  clwlkssizeeq  30012  clwwlknon  30017  clwwlk0on0  30019  konigsberglem5  30183  fusgreg2wsplem  30260  fusgreghash2wsp  30265  2clwwlk  30274  clwwlknonclwlknonen  30290  numclwlk1lem2  30297  numclwwlkovh0  30299  numclwwlkovq  30301  numclwwlkqhash  30302  lnoval  30679  bloval  30708  hmoval  30737  ubthlem1  30797  ubthlem2  30798  ocval  31207  eigvecval  31823  specval  31825  rabfodom  32432  fpwrelmap  32656  nsgmgc  33373  mxidlval  33422  ssmxidl  33435  rprmval  33477  locfinreflem  33817  rspectopn  33844  zarcls1  33846  zarclsun  33847  zarclsiin  33848  zarclsint  33849  zarclssn  33850  zarcls  33851  zartopn  33852  zar0ring  33855  zart0  33856  zarmxt1  33857  zarcmplem  33858  rhmpreimacnlem  33861  rhmpreimacn  33862  ordtconnlem1  33901  sigaex  34087  ddemeas  34213  ismbfm  34228  elunirnmbfm  34229  eulerpart  34360  ballotlem8  34515  reprval  34588  bnj110  34835  fncvm  35225  iscvm  35227  snmlval  35299  satfv1  35331  satfdm  35337  satffunlem1lem2  35371  satfv0fvfmla0  35381  satfv1fvfmla1  35391  mpstval  35503  fvray  36105  icoreval  37317  fin2solem  37576  fin2so  37577  poimirlem4  37594  cnambfre  37638  istotbnd  37739  isbnd  37750  rngohomval  37934  rngoisoval  37947  idlval  37983  pridlval  38003  maxidlval  38009  lshpset  38942  lflset  39023  pats  39249  llnset  39470  lplnset  39494  lvolset  39537  isline  39704  pmapval  39722  paddval  39763  lhpset  39960  ldilset  40074  ltrnset  40083  dilsetN  40118  trnsetN  40121  diaval  40997  diafn  40999  lpolsetN  41447  lcdvadd  41562  lcdsca  41564  lcdvs  41568  mapdval  41593  mapd1o  41613  unitscyglem5  42158  psrmnd  42515  mhmcopsr  42519  mhmcoaddpsr  42520  rhmcomulpsr  42521  evlselv  42557  mhphf  42567  prjcrvval  42602  isnacs  42674  mzpclval  42695  pell1qrval  42816  pell14qrval  42818  pell1234qrval  42820  elmnc  43107  itgoval  43132  idomodle  43162  idomsubgmo  43164  k0004val  44121  permaxsep  44980  icof  45191  elicores  45510  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  stoweidlem34  46011  fourierdlem2  46086  fourierdlem3  46087  etransclem12  46223  etransclem33  46244  ovnval2b  46529  volicorescl  46530  ovncvrrp  46541  ovnsubaddlem1  46547  ovncvr2  46588  issmflem  46704  smfaddlem1  46740  smfaddlem2  46741  smflimlem1  46748  fvmptrabdm  47270  iccpval  47377  fppr  47688  grtri  47900  assintopval  48128  rngchomrnghmresALTV  48202  bigoval  48477  elbigofrcl  48478  line  48660  rrxline  48662  sphere  48675  rrxsphere  48676