Theorem rabex 5309

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 2143  {crab 3416  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564

This theorem is referenced by:  rab2ex  5312  frminex  5640  ssimaex  6966  fvmptrabfv  7022  mptrabex  7223  fnpm  8827  inf3lema  9589  dfac2a  10109  kmlem1  10130  axcc4  10418  axdc3lem2  10430  axdc3lem4  10432  pwfseqlem1  10638  dfuzi  12682  uzval  12859  ixxval  13375  fzval  13532  bitsfval  16476  sadfval  16505  smufval  16530  phicl2  16822  hashgcdeq  16844  prmreclem4  16974  prmreclem5  16975  ismre  17637  fnmre  17638  mrisval  17681  isacs  17702  ismon  17785  isnat  18002  natffn  18004  initofn  18039  termofn  18040  initoval  18045  termoval  18046  coafval  18116  ismgmhm  18749  issubmgm  18755  ismhm  18838  issubm  18856  issubg  19187  isnsg  19216  gimfn  19326  isgim  19327  isga  19356  cntzval  19386  odfval  19597  odngen  19642  gexval  19643  isslw  19673  ablfac1a  20136  ablfac1b  20137  ablfac1c  20138  ablfac1eu  20140  ablfaclem1  20152  ablfaclem2  20153  ablfaclem3  20154  isirred  20497  rnghmfn  20517  rnghmval  20518  isrngim  20523  rhmval0  20553  isrim0  20561  rimfn  20585  issubrng  20646  issubrg  20670  rrgval  20796  issdrg  20891  abvfval  20913  lssset  21054  lmimfn  21147  islmhm  21148  islmim  21183  islbs  21197  ocvval  21817  elocv  21818  isobs  21870  islinds  21959  psrval  22065  psraddcl  22089  psrvscacl  22101  psrgrp  22106  psrlmod  22109  subrgpsr  22127  mvrf  22134  mplsubrg  22154  mplmonmul  22187  mplbas2  22193  opsrval  22197  rhmcomulmpl  22275  mhpval  22302  mhpmulcl  22312  mhpinvcl  22315  psdcl  22324  psdmplcl  22325  psdadd  22326  psdmul  22329  psrplusgpropd  22395  psropprmul  22397  scmatval  22661  fncld  23179  cnfval  23390  cnpval  23393  iscnp2  23396  1stcfb  23602  kgenf  23698  xkoopn  23746  dfac14  23775  hmeofn  23914  hmeofval  23915  filunirn  24039  alexsubALTlem2  24205  ucnval  24433  iscfilu  24444  ispsmet  24461  ismet  24480  isxmet  24481  xmetunirn  24494  cncfval  25047  ishtpy  25131  isphtpy  25140  om1bas  25190  cfilfval  25423  caufval  25434  iscmet  25443  dyadmax  25757  vitalilem2  25768  vitalilem3  25769  vitalilem4  25770  itg2monolem1  25909  fncpn  26092  elcpn  26093  mdeg0  26227  mdegaddle  26231  mdegvsca  26233  uc1pval  26297  mon1pval  26299  aannenlem1  26491  aannenlem2  26492  aannenlem3  26493  vmaval  27277  sqff1o  27346  musum  27355  dchrval  27398  dchrbas  27399  leftval  28042  rightval  28043  leftf  28048  rightf  28049  precsexlem4  28403  precsexlem5  28404  tglnfn  28816  tglnunirn  28817  tglngval  28820  israg  28977  tgplnfn  29057  isplng  29060  iseqlg  29184  ttgitvval  29231  ebtwntg  29332  incistruhgr  29429  usgredgleordALT  29584  vtxdun  29831  vtxdlfgrval  29835  vtxd0nedgb  29838  vtxdushgrfvedglem  29839  vtxdushgrfvedg  29840  vtxdusgr0edgnelALT  29846  1loopgrvd2  29853  usgrvd0nedg  29883  rusgrnumwrdl2  29936  ewlksfval  29951  wwlksn  30186  wspthsn  30197  iswwlksnon  30202  iswspthsnon  30205  wlknwwlksnen  30238  wwlksnexthasheq  30252  rusgrnumwlkg  30329  clwlkclwwlken  30363  clwwlkn  30377  clwwlken  30403  clwlkssizeeq  30436  clwwlknon  30441  clwwlk0on0  30443  konigsberglem5  30607  fusgreg2wsplem  30684  fusgreghash2wsp  30689  2clwwlk  30698  clwwlknonclwlknonen  30714  numclwlk1lem2  30721  numclwwlkovh0  30723  numclwwlkovq  30725  numclwwlkqhash  30726  lnoval  31104  bloval  31133  hmoval  31162  ubthlem1  31222  ubthlem2  31223  ocval  31632  eigvecval  32248  specval  32250  rabfodom  32851  fpwrelmap  33078  nsgmgc  33721  mxidlval  33744  ssmxidl  33757  rprmval  33806  selvply1rhmlem4  33913  evlextv  33932  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  psrmonmul  33940  esplyfval0  33954  esplyfvaln  33964  locfinreflem  34230  rspectopn  34257  zarcls1  34259  zarclsun  34260  zarclsiin  34261  zarclsint  34262  zarclssn  34263  zarcls  34264  zartopn  34265  zar0ring  34268  zart0  34269  zarmxt1  34270  zarcmplem  34271  rhmpreimacnlem  34274  rhmpreimacn  34275  ordtconnlem1  34314  sigaex  34500  ddemeas  34626  ismbfm  34641  elunirnmbfm  34642  eulerpart  34772  ballotlem8  34927  reprval  34997  bnj110  35246  fncvm  35749  iscvm  35751  snmlval  35823  satfv1  35855  satfdm  35861  satffunlem1lem2  35895  satfv0fvfmla0  35905  satfv1fvfmla1  35915  mpstval  36027  fvray  36633  regsfromregtco  37049  icoreval  37999  fin2solem  38257  fin2so  38258  poimirlem4  38275  cnambfre  38319  istotbnd  38420  isbnd  38431  rngohomval  38615  rngoisoval  38628  idlval  38664  pridlval  38684  maxidlval  38690  lshpset  39752  lflset  39833  pats  40059  llnset  40279  lplnset  40303  lvolset  40346  isline  40513  pmapval  40531  paddval  40572  lhpset  40769  ldilset  40883  ltrnset  40892  dilsetN  40927  trnsetN  40930  diaval  41806  diafn  41808  lpolsetN  42256  lcdvadd  42371  lcdsca  42373  lcdvs  42377  mapdval  42402  mapd1o  42422  unitscyglem5  42966  psrmnd  43311  mhmcopsr  43312  mhmcoaddpsr  43313  rhmcomulpsr  43314  evlselv  43321  mhphf  43329  prjcrvval  43364  isnacs  43435  mzpclval  43456  pell1qrval  43573  pell14qrval  43575  pell1234qrval  43577  elmnc  43863  itgoval  43888  idomodle  43918  idomsubgmo  43920  k0004val  44876  permaxsep  45716  icof  45935  elicores  46249  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  stoweidlem34  46748  fourierdlem2  46823  fourierdlem3  46824  etransclem12  46960  etransclem33  46981  ovnval2b  47266  volicorescl  47267  ovncvrrp  47278  ovnsubaddlem1  47284  ovncvr2  47325  issmflem  47441  smfaddlem1  47477  smfaddlem2  47478  smflimlem1  47485  fvmptrabdm  48030  iccpval  48164  fppr  48491  grtri  48705  assintopval  48970  rngchomrnghmresALTV  49044  bigoval  49329  elbigofrcl  49330  line  49512  rrxline  49514  sphere  49527  rrxsphere  49528