Theorem rabex 5280

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

Syntax hints:   ∈ wcel 2114  {crab 3389  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543

This theorem is referenced by:  rab2ex  5283  frminex  5610  ssimaex  6925  fvmptrabfv  6980  mptrabex  7180  fnpm  8781  inf3lema  9545  dfac2a  10052  kmlem1  10073  axcc4  10361  axdc3lem2  10373  axdc3lem4  10375  pwfseqlem1  10581  dfuzi  12620  uzval  12790  ixxval  13306  fzval  13463  bitsfval  16392  sadfval  16421  smufval  16446  phicl2  16738  hashgcdeq  16760  prmreclem4  16890  prmreclem5  16891  ismre  17552  fnmre  17553  mrisval  17596  isacs  17617  ismon  17700  isnat  17917  natffn  17919  initofn  17954  termofn  17955  initoval  17960  termoval  17961  coafval  18031  ismgmhm  18664  issubmgm  18670  ismhm  18753  issubm  18771  issubg  19102  isnsg  19130  gimfn  19236  isgim  19237  isga  19266  cntzval  19296  odfval  19507  odngen  19552  gexval  19553  isslw  19583  ablfac1a  20046  ablfac1b  20047  ablfac1c  20048  ablfac1eu  20050  ablfaclem1  20062  ablfaclem2  20063  ablfaclem3  20064  isirred  20399  rnghmfn  20419  rnghmval  20420  isrngim  20425  isrim0  20462  issubrng  20524  issubrg  20548  rrgval  20674  issdrg  20765  abvfval  20787  lssset  20928  lmimfn  21021  islmhm  21022  islmim  21057  islbs  21071  ocvval  21647  elocv  21648  isobs  21700  islinds  21789  psrval  21895  psraddcl  21918  psrvscacl  21930  psrgrp  21935  psrlmod  21938  subrgpsr  21956  mvrf  21963  mplsubrg  21983  mplmonmul  22014  mplbas2  22020  opsrval  22024  mhpval  22105  mhpmulcl  22115  mhpinvcl  22118  psdcl  22127  psdmplcl  22128  psdadd  22129  psdmul  22132  psrplusgpropd  22199  psropprmul  22201  rhmcomulmpl  22347  scmatval  22469  fncld  22987  cnfval  23198  cnpval  23201  iscnp2  23204  1stcfb  23410  kgenf  23506  xkoopn  23554  dfac14  23583  hmeofn  23722  hmeofval  23723  filunirn  23847  alexsubALTlem2  24013  ucnval  24241  iscfilu  24252  ispsmet  24269  ismet  24288  isxmet  24289  xmetunirn  24302  cncfval  24855  ishtpy  24939  isphtpy  24948  om1bas  24998  cfilfval  25231  caufval  25242  iscmet  25251  dyadmax  25565  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  itg2monolem1  25717  fncpn  25900  elcpn  25901  mdeg0  26035  mdegaddle  26039  mdegvsca  26041  uc1pval  26105  mon1pval  26107  aannenlem1  26294  aannenlem2  26295  aannenlem3  26296  vmaval  27076  sqff1o  27145  musum  27154  dchrval  27197  dchrbas  27198  leftval  27841  rightval  27842  leftf  27847  rightf  27848  precsexlem4  28202  precsexlem5  28203  tglnfn  28615  tglnunirn  28616  tglngval  28619  israg  28765  iseqlg  28935  ttgitvval  28950  ebtwntg  29051  incistruhgr  29148  usgredgleordALT  29303  vtxdun  29550  vtxdlfgrval  29554  vtxd0nedgb  29557  vtxdushgrfvedglem  29558  vtxdushgrfvedg  29559  vtxdusgr0edgnelALT  29565  1loopgrvd2  29572  usgrvd0nedg  29602  rusgrnumwrdl2  29655  ewlksfval  29670  wwlksn  29905  wspthsn  29916  iswwlksnon  29921  iswspthsnon  29924  wlknwwlksnen  29957  wwlksnexthasheq  29971  rusgrnumwlkg  30048  clwlkclwwlken  30082  clwwlkn  30096  clwwlken  30122  clwlkssizeeq  30155  clwwlknon  30160  clwwlk0on0  30162  konigsberglem5  30326  fusgreg2wsplem  30403  fusgreghash2wsp  30408  2clwwlk  30417  clwwlknonclwlknonen  30433  numclwlk1lem2  30440  numclwwlkovh0  30442  numclwwlkovq  30444  numclwwlkqhash  30445  lnoval  30823  bloval  30852  hmoval  30881  ubthlem1  30941  ubthlem2  30942  ocval  31351  eigvecval  31967  specval  31969  rabfodom  32575  fpwrelmap  32806  nsgmgc  33472  mxidlval  33521  ssmxidl  33534  rprmval  33576  evlextv  33686  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonmul  33694  esplyfval0  33708  esplyfvaln  33718  locfinreflem  33984  rspectopn  34011  zarcls1  34013  zarclsun  34014  zarclsiin  34015  zarclsint  34016  zarclssn  34017  zarcls  34018  zartopn  34019  zar0ring  34022  zart0  34023  zarmxt1  34024  zarcmplem  34025  rhmpreimacnlem  34028  rhmpreimacn  34029  ordtconnlem1  34068  sigaex  34254  ddemeas  34380  ismbfm  34395  elunirnmbfm  34396  eulerpart  34526  ballotlem8  34681  reprval  34754  bnj110  35000  fncvm  35439  iscvm  35441  snmlval  35513  satfv1  35545  satfdm  35551  satffunlem1lem2  35585  satfv0fvfmla0  35595  satfv1fvfmla1  35605  mpstval  35717  fvray  36323  regsfromregtco  36720  icoreval  37669  fin2solem  37927  fin2so  37928  poimirlem4  37945  cnambfre  37989  istotbnd  38090  isbnd  38101  rngohomval  38285  rngoisoval  38298  idlval  38334  pridlval  38354  maxidlval  38360  lshpset  39424  lflset  39505  pats  39731  llnset  39951  lplnset  39975  lvolset  40018  isline  40185  pmapval  40203  paddval  40244  lhpset  40441  ldilset  40555  ltrnset  40564  dilsetN  40599  trnsetN  40602  diaval  41478  diafn  41480  lpolsetN  41928  lcdvadd  42043  lcdsca  42045  lcdvs  42049  mapdval  42074  mapd1o  42094  unitscyglem5  42638  psrmnd  42988  mhmcopsr  42992  mhmcoaddpsr  42993  rhmcomulpsr  42994  evlselv  43020  mhphf  43030  prjcrvval  43065  isnacs  43136  mzpclval  43157  pell1qrval  43274  pell14qrval  43276  pell1234qrval  43278  elmnc  43564  itgoval  43589  idomodle  43619  idomsubgmo  43621  k0004val  44577  permaxsep  45434  icof  45648  elicores  45963  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  stoweidlem34  46462  fourierdlem2  46537  fourierdlem3  46538  etransclem12  46674  etransclem33  46695  ovnval2b  46980  volicorescl  46981  ovncvrrp  46992  ovnsubaddlem1  46998  ovncvr2  47039  issmflem  47155  smfaddlem1  47191  smfaddlem2  47192  smflimlem1  47199  fvmptrabdm  47741  iccpval  47875  fppr  48202  grtri  48416  assintopval  48681  rngchomrnghmresALTV  48755  bigoval  49025  elbigofrcl  49026  line  49208  rrxline  49210  sphere  49223  rrxsphere  49224