Theorem rabex 5259

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

Syntax hints:   ∈ wcel 2109  {crab 3069  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  rab2ex  5262  frminex  5568  ssimaex  6847  fvmptrabfv  6900  mptrabex  7095  fnpm  8597  inf3lema  9343  dfac2a  9869  kmlem1  9890  axcc4  10179  axdc3lem2  10191  axdc3lem4  10193  pwfseqlem1  10398  dfuzi  12394  uzval  12566  ixxval  13069  fzval  13223  bitsfval  16111  sadfval  16140  smufval  16165  phicl2  16450  hashgcdeq  16471  prmreclem4  16601  prmreclem5  16602  ismre  17280  fnmre  17281  mrisval  17320  isacs  17341  ismon  17426  isnat  17644  natffn  17646  initofn  17683  termofn  17684  initoval  17689  termoval  17690  coafval  17760  ismhm  18413  issubm  18423  issubg  18736  isnsg  18764  gimfn  18858  isgim  18859  isga  18878  cntzval  18908  odfval  19121  odngen  19163  gexval  19164  isslw  19194  ablfac1a  19653  ablfac1b  19654  ablfac1c  19655  ablfac1eu  19657  ablfaclem1  19669  ablfaclem2  19670  ablfaclem3  19671  isirred  19922  isrim0  19948  issubrg  20005  issdrg  20044  abvfval  20059  lssset  20176  lmimfn  20269  islmhm  20270  islmim  20305  islbs  20319  rrgval  20539  ocvval  20853  elocv  20854  isobs  20908  islinds  20997  psrval  21099  psraddcl  21133  psrvscacl  21143  psrgrp  21148  psrlmod  21151  subrgpsr  21169  mvrf  21174  mplsubrg  21192  mplmonmul  21218  mplbas2  21224  opsrval  21228  mhpval  21311  mhpmulcl  21320  mhpinvcl  21323  psrplusgpropd  21388  psropprmul  21390  scmatval  21634  fncld  22154  cnfval  22365  cnpval  22368  iscnp2  22371  1stcfb  22577  kgenf  22673  xkoopn  22721  dfac14  22750  hmeofn  22889  hmeofval  22890  filunirn  23014  alexsubALTlem2  23180  ucnval  23410  iscfilu  23421  ispsmet  23438  ismet  23457  isxmet  23458  xmetunirn  23471  cncfval  24032  ishtpy  24116  isphtpy  24125  om1bas  24175  cfilfval  24409  caufval  24420  iscmet  24429  dyadmax  24743  vitalilem2  24754  vitalilem3  24755  vitalilem4  24756  itg2monolem1  24896  fncpn  25078  elcpn  25079  mdeg0  25216  mdegaddle  25220  mdegvsca  25222  uc1pval  25285  mon1pval  25287  aannenlem1  25469  aannenlem2  25470  aannenlem3  25471  vmaval  26243  sqff1o  26312  musum  26321  dchrval  26363  dchrbas  26364  tglnfn  26889  tglnunirn  26890  tglngval  26893  israg  27039  iseqlg  27209  ttgitvval  27230  ebtwntg  27331  incistruhgr  27430  usgredgleordALT  27582  vtxdun  27829  vtxdlfgrval  27833  vtxd0nedgb  27836  vtxdushgrfvedglem  27837  vtxdushgrfvedg  27838  vtxdusgr0edgnelALT  27844  1loopgrvd2  27851  usgrvd0nedg  27881  rusgrnumwrdl2  27934  ewlksfval  27949  wwlksn  28181  wspthsn  28192  iswwlksnon  28197  iswspthsnon  28200  wlknwwlksnen  28233  wwlksnexthasheq  28247  rusgrnumwlkg  28321  clwlkclwwlken  28355  clwwlkn  28369  clwwlken  28395  clwlkssizeeq  28428  clwwlknon  28433  clwwlk0on0  28435  konigsberglem5  28599  fusgreg2wsplem  28676  fusgreghash2wsp  28681  2clwwlk  28690  clwwlknonclwlknonen  28706  numclwlk1lem2  28713  numclwwlkovh0  28715  numclwwlkovq  28717  numclwwlkqhash  28718  lnoval  29093  bloval  29122  hmoval  29151  ubthlem1  29211  ubthlem2  29212  ocval  29621  eigvecval  30237  specval  30239  rabfodom  30830  fpwrelmap  31047  nsgmgc  31576  mxidlval  31612  ssmxidl  31621  rprmval  31643  locfinreflem  31769  rspectopn  31796  zarcls1  31798  zarclsun  31799  zarclsiin  31800  zarclsint  31801  zarclssn  31802  zarcls  31803  zartopn  31804  zar0ring  31807  zart0  31808  zarmxt1  31809  zarcmplem  31810  rhmpreimacnlem  31813  rhmpreimacn  31814  ordtconnlem1  31853  sigaex  32057  ddemeas  32183  ismbfm  32198  elunirnmbfm  32199  eulerpart  32328  ballotlem8  32482  reprval  32569  bnj110  32817  fncvm  33198  iscvm  33200  snmlval  33272  satfv1  33304  satfdm  33310  satffunlem1lem2  33344  satfv0fvfmla0  33354  satfv1fvfmla1  33364  mpstval  33476  leftval  34026  rightval  34027  leftf  34028  rightf  34029  fvray  34422  icoreval  35503  fin2solem  35742  fin2so  35743  poimirlem4  35760  cnambfre  35804  istotbnd  35906  isbnd  35917  rngohomval  36101  rngoisoval  36114  idlval  36150  pridlval  36170  maxidlval  36176  lshpset  36971  lflset  37052  pats  37278  llnset  37498  lplnset  37522  lvolset  37565  isline  37732  pmapval  37750  paddval  37791  lhpset  37988  ldilset  38102  ltrnset  38111  dilsetN  38146  trnsetN  38149  diaval  39025  diafn  39027  lpolsetN  39475  lcdvadd  39590  lcdsca  39592  lcdvs  39596  mapdval  39621  mapd1o  39641  selvval2lem4  40208  mhphf  40265  prjcrvval  40449  isnacs  40506  mzpclval  40527  pell1qrval  40648  pell14qrval  40650  pell1234qrval  40652  elmnc  40941  itgoval  40966  idomodle  41001  idomsubgmo  41003  k0004val  41713  icof  42712  elicores  43025  dvnprodlem1  43441  dvnprodlem2  43442  dvnprodlem3  43443  stoweidlem34  43529  fourierdlem2  43604  fourierdlem3  43605  etransclem12  43741  etransclem33  43762  ovnval2b  44044  volicorescl  44045  ovncvrrp  44056  ovnsubaddlem1  44062  ovncvr2  44103  issmflem  44214  smfaddlem1  44249  smfaddlem2  44250  smflimlem1  44257  fvmptrabdm  44736  iccpval  44819  fppr  45130  ismgmhm  45289  issubmgm  45295  assintopval  45351  rnghmfn  45400  rnghmval  45401  isrngisom  45406  rngchomrnghmresALTV  45506  bigoval  45847  elbigofrcl  45848  line  46030  rrxline  46032  sphere  46045  rrxsphere  46046