Theorem rabex 5310

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

Syntax hints:   ∈ wcel 2149  {crab 3423  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-pw 4569

This theorem is referenced by:  rab2ex  5313  frminex  5641  ssimaex  6967  fvmptrabfv  7023  mptrabex  7224  fnpm  8830  inf3lema  9592  dfac2a  10112  kmlem1  10133  axcc4  10422  axdc3lem2  10434  axdc3lem4  10436  pwfseqlem1  10642  dfuzi  12686  uzval  12863  ixxval  13379  fzval  13536  bitsfval  16480  sadfval  16509  smufval  16534  phicl2  16826  hashgcdeq  16848  prmreclem4  16978  prmreclem5  16979  ismre  17641  fnmre  17642  mrisval  17685  isacs  17706  ismon  17789  isnat  18006  natffn  18008  initofn  18043  termofn  18044  initoval  18049  termoval  18050  coafval  18120  ismgmhm  18753  issubmgm  18759  ismhm  18842  issubm  18860  issubg  19191  isnsg  19220  gimfn  19330  isgim  19331  isga  19360  cntzval  19390  odfval  19601  odngen  19646  gexval  19647  isslw  19677  ablfac1a  20140  ablfac1b  20141  ablfac1c  20142  ablfac1eu  20144  ablfaclem1  20156  ablfaclem2  20157  ablfaclem3  20158  isirred  20500  rnghmfn  20520  rnghmval  20521  isrngim  20526  isrim0  20563  issubrng  20631  issubrg  20655  rrgval  20781  issdrg  20868  abvfval  20890  lssset  21031  lmimfn  21124  islmhm  21125  islmim  21160  islbs  21174  ocvval  21785  elocv  21786  isobs  21838  islinds  21927  psrval  22033  psraddcl  22057  psrvscacl  22069  psrgrp  22074  psrlmod  22077  subrgpsr  22095  mvrf  22102  mplsubrg  22122  mplmonmul  22155  mplbas2  22161  opsrval  22165  rhmcomulmpl  22243  mhpval  22270  mhpmulcl  22280  mhpinvcl  22283  psdcl  22292  psdmplcl  22293  psdadd  22294  psdmul  22297  psrplusgpropd  22363  psropprmul  22365  scmatval  22629  fncld  23147  cnfval  23358  cnpval  23361  iscnp2  23364  1stcfb  23570  kgenf  23666  xkoopn  23714  dfac14  23743  hmeofn  23882  hmeofval  23883  filunirn  24007  alexsubALTlem2  24173  ucnval  24401  iscfilu  24412  ispsmet  24429  ismet  24448  isxmet  24449  xmetunirn  24462  cncfval  25015  ishtpy  25099  isphtpy  25108  om1bas  25158  cfilfval  25391  caufval  25402  iscmet  25411  dyadmax  25725  vitalilem2  25736  vitalilem3  25737  vitalilem4  25738  itg2monolem1  25877  fncpn  26060  elcpn  26061  mdeg0  26195  mdegaddle  26199  mdegvsca  26201  uc1pval  26265  mon1pval  26267  aannenlem1  26457  aannenlem2  26458  aannenlem3  26459  vmaval  27242  sqff1o  27311  musum  27320  dchrval  27363  dchrbas  27364  leftval  28007  rightval  28008  leftf  28013  rightf  28014  precsexlem4  28368  precsexlem5  28369  tglnfn  28781  tglnunirn  28782  tglngval  28785  israg  28935  tgplnfn  29014  isplng  29017  iseqlg  29138  ttgitvval  29171  ebtwntg  29272  incistruhgr  29369  usgredgleordALT  29524  vtxdun  29771  vtxdlfgrval  29775  vtxd0nedgb  29778  vtxdushgrfvedglem  29779  vtxdushgrfvedg  29780  vtxdusgr0edgnelALT  29786  1loopgrvd2  29793  usgrvd0nedg  29823  rusgrnumwrdl2  29876  ewlksfval  29891  wwlksn  30126  wspthsn  30137  iswwlksnon  30142  iswspthsnon  30145  wlknwwlksnen  30178  wwlksnexthasheq  30192  rusgrnumwlkg  30269  clwlkclwwlken  30303  clwwlkn  30317  clwwlken  30343  clwlkssizeeq  30376  clwwlknon  30381  clwwlk0on0  30383  konigsberglem5  30547  fusgreg2wsplem  30624  fusgreghash2wsp  30629  2clwwlk  30638  clwwlknonclwlknonen  30654  numclwlk1lem2  30661  numclwwlkovh0  30663  numclwwlkovq  30665  numclwwlkqhash  30666  lnoval  31044  bloval  31073  hmoval  31102  ubthlem1  31162  ubthlem2  31163  ocval  31572  eigvecval  32188  specval  32190  rabfodom  32791  fpwrelmap  33018  nsgmgc  33664  mxidlval  33688  ssmxidl  33701  rprmval  33750  selvply1rhmlem4  33857  evlextv  33876  mplvrpmfgalem  33878  mplvrpmga  33879  mplvrpmmhm  33880  mplvrpmrhm  33881  psrmonmul  33884  esplyfval0  33898  esplyfvaln  33908  locfinreflem  34174  rspectopn  34201  zarcls1  34203  zarclsun  34204  zarclsiin  34205  zarclsint  34206  zarclssn  34207  zarcls  34208  zartopn  34209  zar0ring  34212  zart0  34213  zarmxt1  34214  zarcmplem  34215  rhmpreimacnlem  34218  rhmpreimacn  34219  ordtconnlem1  34258  sigaex  34444  ddemeas  34570  ismbfm  34585  elunirnmbfm  34586  eulerpart  34716  ballotlem8  34871  reprval  34941  bnj110  35190  fncvm  35647  iscvm  35649  snmlval  35721  satfv1  35753  satfdm  35759  satffunlem1lem2  35793  satfv0fvfmla0  35803  satfv1fvfmla1  35813  mpstval  35925  fvray  36531  regsfromregtco  36937  icoreval  37886  fin2solem  38144  fin2so  38145  poimirlem4  38162  cnambfre  38206  istotbnd  38307  isbnd  38318  rngohomval  38502  rngoisoval  38515  idlval  38551  pridlval  38571  maxidlval  38577  lshpset  39641  lflset  39722  pats  39948  llnset  40168  lplnset  40192  lvolset  40235  isline  40402  pmapval  40420  paddval  40461  lhpset  40658  ldilset  40772  ltrnset  40781  dilsetN  40816  trnsetN  40819  diaval  41695  diafn  41697  lpolsetN  42145  lcdvadd  42260  lcdsca  42262  lcdvs  42266  mapdval  42291  mapd1o  42311  unitscyglem5  42855  psrmnd  43202  mhmcopsr  43203  mhmcoaddpsr  43204  rhmcomulpsr  43205  evlselv  43212  mhphf  43220  prjcrvval  43255  isnacs  43326  mzpclval  43347  pell1qrval  43464  pell14qrval  43466  pell1234qrval  43468  elmnc  43754  itgoval  43779  idomodle  43809  idomsubgmo  43811  k0004val  44767  permaxsep  45607  icof  45826  elicores  46140  dvnprodlem1  46551  dvnprodlem2  46552  dvnprodlem3  46553  stoweidlem34  46639  fourierdlem2  46714  fourierdlem3  46715  etransclem12  46851  etransclem33  46872  ovnval2b  47157  volicorescl  47158  ovncvrrp  47169  ovnsubaddlem1  47175  ovncvr2  47216  issmflem  47332  smfaddlem1  47368  smfaddlem2  47369  smflimlem1  47376  fvmptrabdm  47918  iccpval  48052  fppr  48379  grtri  48593  assintopval  48858  rngchomrnghmresALTV  48932  bigoval  49213  elbigofrcl  49214  line  49396  rrxline  49398  sphere  49411  rrxsphere  49412