Theorem rabex 5294

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

Syntax hints:   ∈ wcel 2109  {crab 3405  Vcvv 3447

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  rab2ex  5297  frminex  5617  ssimaex  6946  fvmptrabfv  7000  mptrabex  7199  fnpm  8807  inf3lema  9577  dfac2a  10083  kmlem1  10104  axcc4  10392  axdc3lem2  10404  axdc3lem4  10406  pwfseqlem1  10611  dfuzi  12625  uzval  12795  ixxval  13314  fzval  13470  bitsfval  16393  sadfval  16422  smufval  16447  phicl2  16738  hashgcdeq  16760  prmreclem4  16890  prmreclem5  16891  ismre  17551  fnmre  17552  mrisval  17591  isacs  17612  ismon  17695  isnat  17912  natffn  17914  initofn  17949  termofn  17950  initoval  17955  termoval  17956  coafval  18026  ismgmhm  18623  issubmgm  18629  ismhm  18712  issubm  18730  issubg  19058  isnsg  19087  gimfn  19193  isgim  19194  isga  19223  cntzval  19253  odfval  19462  odngen  19507  gexval  19508  isslw  19538  ablfac1a  20001  ablfac1b  20002  ablfac1c  20003  ablfac1eu  20005  ablfaclem1  20017  ablfaclem2  20018  ablfaclem3  20019  isirred  20328  rnghmfn  20348  rnghmval  20349  isrngim  20354  isrim0OLD  20390  isrim0  20392  issubrng  20456  issubrg  20480  rrgval  20606  issdrg  20697  abvfval  20719  lssset  20839  lmimfn  20933  islmhm  20934  islmim  20969  islbs  20983  ocvval  21576  elocv  21577  isobs  21629  islinds  21718  psrval  21824  psraddcl  21847  psraddclOLD  21848  psrvscacl  21860  psrgrp  21865  psrgrpOLD  21866  psrlmod  21869  subrgpsr  21887  mvrf  21894  mplsubrg  21914  mplmonmul  21943  mplbas2  21949  opsrval  21953  mhpval  22026  mhpmulcl  22036  mhpinvcl  22039  psdcl  22048  psdmplcl  22049  psdadd  22050  psdmul  22053  psrplusgpropd  22120  psropprmul  22122  rhmcomulmpl  22269  scmatval  22391  fncld  22909  cnfval  23120  cnpval  23123  iscnp2  23126  1stcfb  23332  kgenf  23428  xkoopn  23476  dfac14  23505  hmeofn  23644  hmeofval  23645  filunirn  23769  alexsubALTlem2  23935  ucnval  24164  iscfilu  24175  ispsmet  24192  ismet  24211  isxmet  24212  xmetunirn  24225  cncfval  24781  ishtpy  24871  isphtpy  24880  om1bas  24931  cfilfval  25164  caufval  25175  iscmet  25184  dyadmax  25499  vitalilem2  25510  vitalilem3  25511  vitalilem4  25512  itg2monolem1  25651  fncpn  25835  elcpn  25836  mdeg0  25975  mdegaddle  25979  mdegvsca  25981  uc1pval  26045  mon1pval  26047  aannenlem1  26236  aannenlem2  26237  aannenlem3  26238  vmaval  27023  sqff1o  27092  musum  27101  dchrval  27145  dchrbas  27146  leftval  27771  rightval  27772  leftf  27777  rightf  27778  precsexlem4  28112  precsexlem5  28113  tglnfn  28474  tglnunirn  28475  tglngval  28478  israg  28624  iseqlg  28794  ttgitvval  28809  ebtwntg  28909  incistruhgr  29006  usgredgleordALT  29161  vtxdun  29409  vtxdlfgrval  29413  vtxd0nedgb  29416  vtxdushgrfvedglem  29417  vtxdushgrfvedg  29418  vtxdusgr0edgnelALT  29424  1loopgrvd2  29431  usgrvd0nedg  29461  rusgrnumwrdl2  29514  ewlksfval  29529  wwlksn  29767  wspthsn  29778  iswwlksnon  29783  iswspthsnon  29786  wlknwwlksnen  29819  wwlksnexthasheq  29833  rusgrnumwlkg  29907  clwlkclwwlken  29941  clwwlkn  29955  clwwlken  29981  clwlkssizeeq  30014  clwwlknon  30019  clwwlk0on0  30021  konigsberglem5  30185  fusgreg2wsplem  30262  fusgreghash2wsp  30267  2clwwlk  30276  clwwlknonclwlknonen  30292  numclwlk1lem2  30299  numclwwlkovh0  30301  numclwwlkovq  30303  numclwwlkqhash  30304  lnoval  30681  bloval  30710  hmoval  30739  ubthlem1  30799  ubthlem2  30800  ocval  31209  eigvecval  31825  specval  31827  rabfodom  32434  fpwrelmap  32656  nsgmgc  33383  mxidlval  33432  ssmxidl  33445  rprmval  33487  locfinreflem  33830  rspectopn  33857  zarcls1  33859  zarclsun  33860  zarclsiin  33861  zarclsint  33862  zarclssn  33863  zarcls  33864  zartopn  33865  zar0ring  33868  zart0  33869  zarmxt1  33870  zarcmplem  33871  rhmpreimacnlem  33874  rhmpreimacn  33875  ordtconnlem1  33914  sigaex  34100  ddemeas  34226  ismbfm  34241  elunirnmbfm  34242  eulerpart  34373  ballotlem8  34528  reprval  34601  bnj110  34848  fncvm  35244  iscvm  35246  snmlval  35318  satfv1  35350  satfdm  35356  satffunlem1lem2  35390  satfv0fvfmla0  35400  satfv1fvfmla1  35410  mpstval  35522  fvray  36129  icoreval  37341  fin2solem  37600  fin2so  37601  poimirlem4  37618  cnambfre  37662  istotbnd  37763  isbnd  37774  rngohomval  37958  rngoisoval  37971  idlval  38007  pridlval  38027  maxidlval  38033  lshpset  38971  lflset  39052  pats  39278  llnset  39499  lplnset  39523  lvolset  39566  isline  39733  pmapval  39751  paddval  39792  lhpset  39989  ldilset  40103  ltrnset  40112  dilsetN  40147  trnsetN  40150  diaval  41026  diafn  41028  lpolsetN  41476  lcdvadd  41591  lcdsca  41593  lcdvs  41597  mapdval  41622  mapd1o  41642  unitscyglem5  42187  psrmnd  42533  mhmcopsr  42537  mhmcoaddpsr  42538  rhmcomulpsr  42539  evlselv  42575  mhphf  42585  prjcrvval  42620  isnacs  42692  mzpclval  42713  pell1qrval  42834  pell14qrval  42836  pell1234qrval  42838  elmnc  43125  itgoval  43150  idomodle  43180  idomsubgmo  43182  k0004val  44139  permaxsep  44997  icof  45213  elicores  45531  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  stoweidlem34  46032  fourierdlem2  46107  fourierdlem3  46108  etransclem12  46244  etransclem33  46265  ovnval2b  46550  volicorescl  46551  ovncvrrp  46562  ovnsubaddlem1  46568  ovncvr2  46609  issmflem  46725  smfaddlem1  46761  smfaddlem2  46762  smflimlem1  46769  fvmptrabdm  47294  iccpval  47416  fppr  47727  grtri  47939  assintopval  48193  rngchomrnghmresALTV  48267  bigoval  48538  elbigofrcl  48539  line  48721  rrxline  48723  sphere  48736  rrxsphere  48737