Theorem rabex 5289

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

Syntax hints:   ∈ wcel 2109  {crab 3402  Vcvv 3444

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 5246

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 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  rab2ex  5292  frminex  5610  ssimaex  6928  fvmptrabfv  6982  mptrabex  7181  fnpm  8784  inf3lema  9553  dfac2a  10059  kmlem1  10080  axcc4  10368  axdc3lem2  10380  axdc3lem4  10382  pwfseqlem1  10587  dfuzi  12601  uzval  12771  ixxval  13290  fzval  13446  bitsfval  16369  sadfval  16398  smufval  16423  phicl2  16714  hashgcdeq  16736  prmreclem4  16866  prmreclem5  16867  ismre  17527  fnmre  17528  mrisval  17571  isacs  17592  ismon  17675  isnat  17892  natffn  17894  initofn  17929  termofn  17930  initoval  17935  termoval  17936  coafval  18006  ismgmhm  18605  issubmgm  18611  ismhm  18694  issubm  18712  issubg  19040  isnsg  19069  gimfn  19175  isgim  19176  isga  19205  cntzval  19235  odfval  19446  odngen  19491  gexval  19492  isslw  19522  ablfac1a  19985  ablfac1b  19986  ablfac1c  19987  ablfac1eu  19989  ablfaclem1  20001  ablfaclem2  20002  ablfaclem3  20003  isirred  20339  rnghmfn  20359  rnghmval  20360  isrngim  20365  isrim0OLD  20401  isrim0  20403  issubrng  20467  issubrg  20491  rrgval  20617  issdrg  20708  abvfval  20730  lssset  20871  lmimfn  20965  islmhm  20966  islmim  21001  islbs  21015  ocvval  21609  elocv  21610  isobs  21662  islinds  21751  psrval  21857  psraddcl  21880  psraddclOLD  21881  psrvscacl  21893  psrgrp  21898  psrgrpOLD  21899  psrlmod  21902  subrgpsr  21920  mvrf  21927  mplsubrg  21947  mplmonmul  21976  mplbas2  21982  opsrval  21986  mhpval  22059  mhpmulcl  22069  mhpinvcl  22072  psdcl  22081  psdmplcl  22082  psdadd  22083  psdmul  22086  psrplusgpropd  22153  psropprmul  22155  rhmcomulmpl  22302  scmatval  22424  fncld  22942  cnfval  23153  cnpval  23156  iscnp2  23159  1stcfb  23365  kgenf  23461  xkoopn  23509  dfac14  23538  hmeofn  23677  hmeofval  23678  filunirn  23802  alexsubALTlem2  23968  ucnval  24197  iscfilu  24208  ispsmet  24225  ismet  24244  isxmet  24245  xmetunirn  24258  cncfval  24814  ishtpy  24904  isphtpy  24913  om1bas  24964  cfilfval  25197  caufval  25208  iscmet  25217  dyadmax  25532  vitalilem2  25543  vitalilem3  25544  vitalilem4  25545  itg2monolem1  25684  fncpn  25868  elcpn  25869  mdeg0  26008  mdegaddle  26012  mdegvsca  26014  uc1pval  26078  mon1pval  26080  aannenlem1  26269  aannenlem2  26270  aannenlem3  26271  vmaval  27056  sqff1o  27125  musum  27134  dchrval  27178  dchrbas  27179  leftval  27808  rightval  27809  leftf  27814  rightf  27815  precsexlem4  28152  precsexlem5  28153  tglnfn  28527  tglnunirn  28528  tglngval  28531  israg  28677  iseqlg  28847  ttgitvval  28862  ebtwntg  28962  incistruhgr  29059  usgredgleordALT  29214  vtxdun  29462  vtxdlfgrval  29466  vtxd0nedgb  29469  vtxdushgrfvedglem  29470  vtxdushgrfvedg  29471  vtxdusgr0edgnelALT  29477  1loopgrvd2  29484  usgrvd0nedg  29514  rusgrnumwrdl2  29567  ewlksfval  29582  wwlksn  29817  wspthsn  29828  iswwlksnon  29833  iswspthsnon  29836  wlknwwlksnen  29869  wwlksnexthasheq  29883  rusgrnumwlkg  29957  clwlkclwwlken  29991  clwwlkn  30005  clwwlken  30031  clwlkssizeeq  30064  clwwlknon  30069  clwwlk0on0  30071  konigsberglem5  30235  fusgreg2wsplem  30312  fusgreghash2wsp  30317  2clwwlk  30326  clwwlknonclwlknonen  30342  numclwlk1lem2  30349  numclwwlkovh0  30351  numclwwlkovq  30353  numclwwlkqhash  30354  lnoval  30731  bloval  30760  hmoval  30789  ubthlem1  30849  ubthlem2  30850  ocval  31259  eigvecval  31875  specval  31877  rabfodom  32484  fpwrelmap  32706  nsgmgc  33376  mxidlval  33425  ssmxidl  33438  rprmval  33480  locfinreflem  33823  rspectopn  33850  zarcls1  33852  zarclsun  33853  zarclsiin  33854  zarclsint  33855  zarclssn  33856  zarcls  33857  zartopn  33858  zar0ring  33861  zart0  33862  zarmxt1  33863  zarcmplem  33864  rhmpreimacnlem  33867  rhmpreimacn  33868  ordtconnlem1  33907  sigaex  34093  ddemeas  34219  ismbfm  34234  elunirnmbfm  34235  eulerpart  34366  ballotlem8  34521  reprval  34594  bnj110  34841  fncvm  35237  iscvm  35239  snmlval  35311  satfv1  35343  satfdm  35349  satffunlem1lem2  35383  satfv0fvfmla0  35393  satfv1fvfmla1  35403  mpstval  35515  fvray  36122  icoreval  37334  fin2solem  37593  fin2so  37594  poimirlem4  37611  cnambfre  37655  istotbnd  37756  isbnd  37767  rngohomval  37951  rngoisoval  37964  idlval  38000  pridlval  38020  maxidlval  38026  lshpset  38964  lflset  39045  pats  39271  llnset  39492  lplnset  39516  lvolset  39559  isline  39726  pmapval  39744  paddval  39785  lhpset  39982  ldilset  40096  ltrnset  40105  dilsetN  40140  trnsetN  40143  diaval  41019  diafn  41021  lpolsetN  41469  lcdvadd  41584  lcdsca  41586  lcdvs  41590  mapdval  41615  mapd1o  41635  unitscyglem5  42180  psrmnd  42526  mhmcopsr  42530  mhmcoaddpsr  42531  rhmcomulpsr  42532  evlselv  42568  mhphf  42578  prjcrvval  42613  isnacs  42685  mzpclval  42706  pell1qrval  42827  pell14qrval  42829  pell1234qrval  42831  elmnc  43118  itgoval  43143  idomodle  43173  idomsubgmo  43175  k0004val  44132  permaxsep  44990  icof  45206  elicores  45524  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  stoweidlem34  46025  fourierdlem2  46100  fourierdlem3  46101  etransclem12  46237  etransclem33  46258  ovnval2b  46543  volicorescl  46544  ovncvrrp  46555  ovnsubaddlem1  46561  ovncvr2  46602  issmflem  46718  smfaddlem1  46754  smfaddlem2  46755  smflimlem1  46762  fvmptrabdm  47287  iccpval  47409  fppr  47720  grtri  47932  assintopval  48186  rngchomrnghmresALTV  48260  bigoval  48531  elbigofrcl  48532  line  48714  rrxline  48716  sphere  48729  rrxsphere  48730