Theorem rabex 5275

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

Syntax hints:   ∈ wcel 2111  {crab 3395  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4549

This theorem is referenced by:  rab2ex  5278  frminex  5593  ssimaex  6907  fvmptrabfv  6961  mptrabex  7159  fnpm  8758  inf3lema  9514  dfac2a  10021  kmlem1  10042  axcc4  10330  axdc3lem2  10342  axdc3lem4  10344  pwfseqlem1  10549  dfuzi  12564  uzval  12734  ixxval  13253  fzval  13409  bitsfval  16334  sadfval  16363  smufval  16388  phicl2  16679  hashgcdeq  16701  prmreclem4  16831  prmreclem5  16832  ismre  17492  fnmre  17493  mrisval  17536  isacs  17557  ismon  17640  isnat  17857  natffn  17859  initofn  17894  termofn  17895  initoval  17900  termoval  17901  coafval  17971  ismgmhm  18604  issubmgm  18610  ismhm  18693  issubm  18711  issubg  19039  isnsg  19067  gimfn  19173  isgim  19174  isga  19203  cntzval  19233  odfval  19444  odngen  19489  gexval  19490  isslw  19520  ablfac1a  19983  ablfac1b  19984  ablfac1c  19985  ablfac1eu  19987  ablfaclem1  19999  ablfaclem2  20000  ablfaclem3  20001  isirred  20337  rnghmfn  20357  rnghmval  20358  isrngim  20363  isrim0  20400  issubrng  20462  issubrg  20486  rrgval  20612  issdrg  20703  abvfval  20725  lssset  20866  lmimfn  20960  islmhm  20961  islmim  20996  islbs  21010  ocvval  21604  elocv  21605  isobs  21657  islinds  21746  psrval  21852  psraddcl  21875  psraddclOLD  21876  psrvscacl  21888  psrgrp  21893  psrgrpOLD  21894  psrlmod  21897  subrgpsr  21915  mvrf  21922  mplsubrg  21942  mplmonmul  21971  mplbas2  21977  opsrval  21981  mhpval  22054  mhpmulcl  22064  mhpinvcl  22067  psdcl  22076  psdmplcl  22077  psdadd  22078  psdmul  22081  psrplusgpropd  22148  psropprmul  22150  rhmcomulmpl  22297  scmatval  22419  fncld  22937  cnfval  23148  cnpval  23151  iscnp2  23154  1stcfb  23360  kgenf  23456  xkoopn  23504  dfac14  23533  hmeofn  23672  hmeofval  23673  filunirn  23797  alexsubALTlem2  23963  ucnval  24191  iscfilu  24202  ispsmet  24219  ismet  24238  isxmet  24239  xmetunirn  24252  cncfval  24808  ishtpy  24898  isphtpy  24907  om1bas  24958  cfilfval  25191  caufval  25202  iscmet  25211  dyadmax  25526  vitalilem2  25537  vitalilem3  25538  vitalilem4  25539  itg2monolem1  25678  fncpn  25862  elcpn  25863  mdeg0  26002  mdegaddle  26006  mdegvsca  26008  uc1pval  26072  mon1pval  26074  aannenlem1  26263  aannenlem2  26264  aannenlem3  26265  vmaval  27050  sqff1o  27119  musum  27128  dchrval  27172  dchrbas  27173  leftval  27804  rightval  27805  leftf  27810  rightf  27811  precsexlem4  28148  precsexlem5  28149  tglnfn  28525  tglnunirn  28526  tglngval  28529  israg  28675  iseqlg  28845  ttgitvval  28860  ebtwntg  28960  incistruhgr  29057  usgredgleordALT  29212  vtxdun  29460  vtxdlfgrval  29464  vtxd0nedgb  29467  vtxdushgrfvedglem  29468  vtxdushgrfvedg  29469  vtxdusgr0edgnelALT  29475  1loopgrvd2  29482  usgrvd0nedg  29512  rusgrnumwrdl2  29565  ewlksfval  29580  wwlksn  29815  wspthsn  29826  iswwlksnon  29831  iswspthsnon  29834  wlknwwlksnen  29867  wwlksnexthasheq  29881  rusgrnumwlkg  29958  clwlkclwwlken  29992  clwwlkn  30006  clwwlken  30032  clwlkssizeeq  30065  clwwlknon  30070  clwwlk0on0  30072  konigsberglem5  30236  fusgreg2wsplem  30313  fusgreghash2wsp  30318  2clwwlk  30327  clwwlknonclwlknonen  30343  numclwlk1lem2  30350  numclwwlkovh0  30352  numclwwlkovq  30354  numclwwlkqhash  30355  lnoval  30732  bloval  30761  hmoval  30790  ubthlem1  30850  ubthlem2  30851  ocval  31260  eigvecval  31876  specval  31878  rabfodom  32485  fpwrelmap  32716  nsgmgc  33377  mxidlval  33426  ssmxidl  33439  rprmval  33481  mplvrpmfgalem  33574  mplvrpmga  33575  mplvrpmmhm  33576  mplvrpmrhm  33577  locfinreflem  33853  rspectopn  33880  zarcls1  33882  zarclsun  33883  zarclsiin  33884  zarclsint  33885  zarclssn  33886  zarcls  33887  zartopn  33888  zar0ring  33891  zart0  33892  zarmxt1  33893  zarcmplem  33894  rhmpreimacnlem  33897  rhmpreimacn  33898  ordtconnlem1  33937  sigaex  34123  ddemeas  34249  ismbfm  34264  elunirnmbfm  34265  eulerpart  34395  ballotlem8  34550  reprval  34623  bnj110  34870  fncvm  35301  iscvm  35303  snmlval  35375  satfv1  35407  satfdm  35413  satffunlem1lem2  35447  satfv0fvfmla0  35457  satfv1fvfmla1  35467  mpstval  35579  fvray  36183  icoreval  37395  fin2solem  37654  fin2so  37655  poimirlem4  37672  cnambfre  37716  istotbnd  37817  isbnd  37828  rngohomval  38012  rngoisoval  38025  idlval  38061  pridlval  38081  maxidlval  38087  lshpset  39025  lflset  39106  pats  39332  llnset  39552  lplnset  39576  lvolset  39619  isline  39786  pmapval  39804  paddval  39845  lhpset  40042  ldilset  40156  ltrnset  40165  dilsetN  40200  trnsetN  40203  diaval  41079  diafn  41081  lpolsetN  41529  lcdvadd  41644  lcdsca  41646  lcdvs  41650  mapdval  41675  mapd1o  41695  unitscyglem5  42240  psrmnd  42586  mhmcopsr  42590  mhmcoaddpsr  42591  rhmcomulpsr  42592  evlselv  42628  mhphf  42638  prjcrvval  42673  isnacs  42745  mzpclval  42766  pell1qrval  42887  pell14qrval  42889  pell1234qrval  42891  elmnc  43177  itgoval  43202  idomodle  43232  idomsubgmo  43234  k0004val  44191  permaxsep  45048  icof  45264  elicores  45581  dvnprodlem1  45992  dvnprodlem2  45993  dvnprodlem3  45994  stoweidlem34  46080  fourierdlem2  46155  fourierdlem3  46156  etransclem12  46292  etransclem33  46313  ovnval2b  46598  volicorescl  46599  ovncvrrp  46610  ovnsubaddlem1  46616  ovncvr2  46657  issmflem  46773  smfaddlem1  46809  smfaddlem2  46810  smflimlem1  46817  fvmptrabdm  47332  iccpval  47454  fppr  47765  grtri  47979  assintopval  48244  rngchomrnghmresALTV  48318  bigoval  48589  elbigofrcl  48590  line  48772  rrxline  48774  sphere  48787  rrxsphere  48788