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

Syntax hints:   ∈ wcel 2106  {crab 3405  Vcvv 3446

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  rab2ex  5297  frminex  5618  ssimaex  6931  fvmptrabfv  6984  mptrabex  7180  fnpm  8780  inf3lema  9569  dfac2a  10074  kmlem1  10095  axcc4  10384  axdc3lem2  10396  axdc3lem4  10398  pwfseqlem1  10603  dfuzi  12603  uzval  12774  ixxval  13282  fzval  13436  bitsfval  16314  sadfval  16343  smufval  16368  phicl2  16651  hashgcdeq  16672  prmreclem4  16802  prmreclem5  16803  ismre  17484  fnmre  17485  mrisval  17524  isacs  17545  ismon  17630  isnat  17848  natffn  17850  initofn  17887  termofn  17888  initoval  17893  termoval  17894  coafval  17964  ismhm  18617  issubm  18628  issubg  18942  isnsg  18971  gimfn  19065  isgim  19066  isga  19085  cntzval  19115  odfval  19328  odngen  19373  gexval  19374  isslw  19404  ablfac1a  19862  ablfac1b  19863  ablfac1c  19864  ablfac1eu  19866  ablfaclem1  19878  ablfaclem2  19879  ablfaclem3  19880  isirred  20144  isrim0OLD  20170  isrim0  20172  issubrg  20270  issdrg  20311  abvfval  20333  lssset  20451  lmimfn  20544  islmhm  20545  islmim  20580  islbs  20594  rrgval  20794  ocvval  21108  elocv  21109  isobs  21163  islinds  21252  psrval  21354  psraddcl  21388  psrvscacl  21398  psrgrp  21403  psrgrpOLD  21404  psrlmod  21407  subrgpsr  21425  mvrf  21430  mplsubrg  21448  mplmonmul  21474  mplbas2  21480  opsrval  21484  mhpval  21567  mhpmulcl  21576  mhpinvcl  21579  psrplusgpropd  21644  psropprmul  21646  scmatval  21890  fncld  22410  cnfval  22621  cnpval  22624  iscnp2  22627  1stcfb  22833  kgenf  22929  xkoopn  22977  dfac14  23006  hmeofn  23145  hmeofval  23146  filunirn  23270  alexsubALTlem2  23436  ucnval  23666  iscfilu  23677  ispsmet  23694  ismet  23713  isxmet  23714  xmetunirn  23727  cncfval  24288  ishtpy  24372  isphtpy  24381  om1bas  24431  cfilfval  24665  caufval  24676  iscmet  24685  dyadmax  24999  vitalilem2  25010  vitalilem3  25011  vitalilem4  25012  itg2monolem1  25152  fncpn  25334  elcpn  25335  mdeg0  25472  mdegaddle  25476  mdegvsca  25478  uc1pval  25541  mon1pval  25543  aannenlem1  25725  aannenlem2  25726  aannenlem3  25727  vmaval  26499  sqff1o  26568  musum  26577  dchrval  26619  dchrbas  26620  leftval  27236  rightval  27237  leftf  27238  rightf  27239  tglnfn  27552  tglnunirn  27553  tglngval  27556  israg  27702  iseqlg  27872  ttgitvval  27893  ebtwntg  27994  incistruhgr  28093  usgredgleordALT  28245  vtxdun  28492  vtxdlfgrval  28496  vtxd0nedgb  28499  vtxdushgrfvedglem  28500  vtxdushgrfvedg  28501  vtxdusgr0edgnelALT  28507  1loopgrvd2  28514  usgrvd0nedg  28544  rusgrnumwrdl2  28597  ewlksfval  28612  wwlksn  28845  wspthsn  28856  iswwlksnon  28861  iswspthsnon  28864  wlknwwlksnen  28897  wwlksnexthasheq  28911  rusgrnumwlkg  28985  clwlkclwwlken  29019  clwwlkn  29033  clwwlken  29059  clwlkssizeeq  29092  clwwlknon  29097  clwwlk0on0  29099  konigsberglem5  29263  fusgreg2wsplem  29340  fusgreghash2wsp  29345  2clwwlk  29354  clwwlknonclwlknonen  29370  numclwlk1lem2  29377  numclwwlkovh0  29379  numclwwlkovq  29381  numclwwlkqhash  29382  lnoval  29757  bloval  29786  hmoval  29815  ubthlem1  29875  ubthlem2  29876  ocval  30285  eigvecval  30901  specval  30903  rabfodom  31496  fpwrelmap  31718  nsgmgc  32264  mxidlval  32306  ssmxidl  32315  rprmval  32337  locfinreflem  32510  rspectopn  32537  zarcls1  32539  zarclsun  32540  zarclsiin  32541  zarclsint  32542  zarclssn  32543  zarcls  32544  zartopn  32545  zar0ring  32548  zart0  32549  zarmxt1  32550  zarcmplem  32551  rhmpreimacnlem  32554  rhmpreimacn  32555  ordtconnlem1  32594  sigaex  32798  ddemeas  32924  ismbfm  32939  elunirnmbfm  32940  eulerpart  33071  ballotlem8  33225  reprval  33312  bnj110  33559  fncvm  33938  iscvm  33940  snmlval  34012  satfv1  34044  satfdm  34050  satffunlem1lem2  34084  satfv0fvfmla0  34094  satfv1fvfmla1  34104  mpstval  34216  fvray  34802  icoreval  35897  fin2solem  36137  fin2so  36138  poimirlem4  36155  cnambfre  36199  istotbnd  36301  isbnd  36312  rngohomval  36496  rngoisoval  36509  idlval  36545  pridlval  36565  maxidlval  36571  lshpset  37513  lflset  37594  pats  37820  llnset  38041  lplnset  38065  lvolset  38108  isline  38275  pmapval  38293  paddval  38334  lhpset  38531  ldilset  38645  ltrnset  38654  dilsetN  38689  trnsetN  38692  diaval  39568  diafn  39570  lpolsetN  40018  lcdvadd  40133  lcdsca  40135  lcdvs  40139  mapdval  40164  mapd1o  40184  mhmcompl  40794  mhmcoaddmpl  40797  rhmcomulmpl  40798  mhphf  40829  prjcrvval  41028  isnacs  41085  mzpclval  41106  pell1qrval  41227  pell14qrval  41229  pell1234qrval  41231  elmnc  41521  itgoval  41546  idomodle  41581  idomsubgmo  41583  k0004val  42544  icof  43561  elicores  43891  dvnprodlem1  44307  dvnprodlem2  44308  dvnprodlem3  44309  stoweidlem34  44395  fourierdlem2  44470  fourierdlem3  44471  etransclem12  44607  etransclem33  44628  ovnval2b  44913  volicorescl  44914  ovncvrrp  44925  ovnsubaddlem1  44931  ovncvr2  44972  issmflem  45088  smfaddlem1  45124  smfaddlem2  45125  smflimlem1  45132  fvmptrabdm  45645  iccpval  45727  fppr  46038  ismgmhm  46197  issubmgm  46203  assintopval  46259  rnghmfn  46308  rnghmval  46309  isrngisom  46314  rngchomrnghmresALTV  46414  bigoval  46755  elbigofrcl  46756  line  46938  rrxline  46940  sphere  46953  rrxsphere  46954