Theorem rabex 5339

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

Syntax hints:   ∈ wcel 2108  {crab 3436  Vcvv 3480

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  rab2ex  5342  frminex  5664  ssimaex  6994  fvmptrabfv  7048  mptrabex  7245  fnpm  8874  inf3lema  9664  dfac2a  10170  kmlem1  10191  axcc4  10479  axdc3lem2  10491  axdc3lem4  10493  pwfseqlem1  10698  dfuzi  12709  uzval  12880  ixxval  13395  fzval  13549  bitsfval  16460  sadfval  16489  smufval  16514  phicl2  16805  hashgcdeq  16827  prmreclem4  16957  prmreclem5  16958  ismre  17633  fnmre  17634  mrisval  17673  isacs  17694  ismon  17777  isnat  17995  natffn  17997  initofn  18032  termofn  18033  initoval  18038  termoval  18039  coafval  18109  ismgmhm  18709  issubmgm  18715  ismhm  18798  issubm  18816  issubg  19144  isnsg  19173  gimfn  19279  isgim  19280  isga  19309  cntzval  19339  odfval  19550  odngen  19595  gexval  19596  isslw  19626  ablfac1a  20089  ablfac1b  20090  ablfac1c  20091  ablfac1eu  20093  ablfaclem1  20105  ablfaclem2  20106  ablfaclem3  20107  isirred  20419  rnghmfn  20439  rnghmval  20440  isrngim  20445  isrim0OLD  20481  isrim0  20483  issubrng  20547  issubrg  20571  rrgval  20697  issdrg  20789  abvfval  20811  lssset  20931  lmimfn  21025  islmhm  21026  islmim  21061  islbs  21075  ocvval  21685  elocv  21686  isobs  21740  islinds  21829  psrval  21935  psraddcl  21958  psraddclOLD  21959  psrvscacl  21971  psrgrp  21976  psrgrpOLD  21977  psrlmod  21980  subrgpsr  21998  mvrf  22005  mplsubrg  22025  mplmonmul  22054  mplbas2  22060  opsrval  22064  mhpval  22143  mhpmulcl  22153  mhpinvcl  22156  psdcl  22165  psdmplcl  22166  psdadd  22167  psdmul  22170  psrplusgpropd  22237  psropprmul  22239  rhmcomulmpl  22386  scmatval  22510  fncld  23030  cnfval  23241  cnpval  23244  iscnp2  23247  1stcfb  23453  kgenf  23549  xkoopn  23597  dfac14  23626  hmeofn  23765  hmeofval  23766  filunirn  23890  alexsubALTlem2  24056  ucnval  24286  iscfilu  24297  ispsmet  24314  ismet  24333  isxmet  24334  xmetunirn  24347  cncfval  24914  ishtpy  25004  isphtpy  25013  om1bas  25064  cfilfval  25298  caufval  25309  iscmet  25318  dyadmax  25633  vitalilem2  25644  vitalilem3  25645  vitalilem4  25646  itg2monolem1  25785  fncpn  25969  elcpn  25970  mdeg0  26109  mdegaddle  26113  mdegvsca  26115  uc1pval  26179  mon1pval  26181  aannenlem1  26370  aannenlem2  26371  aannenlem3  26372  vmaval  27156  sqff1o  27225  musum  27234  dchrval  27278  dchrbas  27279  leftval  27902  rightval  27903  leftf  27904  rightf  27905  precsexlem4  28234  precsexlem5  28235  tglnfn  28555  tglnunirn  28556  tglngval  28559  israg  28705  iseqlg  28875  ttgitvval  28896  ebtwntg  28997  incistruhgr  29096  usgredgleordALT  29251  vtxdun  29499  vtxdlfgrval  29503  vtxd0nedgb  29506  vtxdushgrfvedglem  29507  vtxdushgrfvedg  29508  vtxdusgr0edgnelALT  29514  1loopgrvd2  29521  usgrvd0nedg  29551  rusgrnumwrdl2  29604  ewlksfval  29619  wwlksn  29857  wspthsn  29868  iswwlksnon  29873  iswspthsnon  29876  wlknwwlksnen  29909  wwlksnexthasheq  29923  rusgrnumwlkg  29997  clwlkclwwlken  30031  clwwlkn  30045  clwwlken  30071  clwlkssizeeq  30104  clwwlknon  30109  clwwlk0on0  30111  konigsberglem5  30275  fusgreg2wsplem  30352  fusgreghash2wsp  30357  2clwwlk  30366  clwwlknonclwlknonen  30382  numclwlk1lem2  30389  numclwwlkovh0  30391  numclwwlkovq  30393  numclwwlkqhash  30394  lnoval  30771  bloval  30800  hmoval  30829  ubthlem1  30889  ubthlem2  30890  ocval  31299  eigvecval  31915  specval  31917  rabfodom  32524  fpwrelmap  32744  nsgmgc  33440  mxidlval  33489  ssmxidl  33502  rprmval  33544  locfinreflem  33839  rspectopn  33866  zarcls1  33868  zarclsun  33869  zarclsiin  33870  zarclsint  33871  zarclssn  33872  zarcls  33873  zartopn  33874  zar0ring  33877  zart0  33878  zarmxt1  33879  zarcmplem  33880  rhmpreimacnlem  33883  rhmpreimacn  33884  ordtconnlem1  33923  sigaex  34111  ddemeas  34237  ismbfm  34252  elunirnmbfm  34253  eulerpart  34384  ballotlem8  34539  reprval  34625  bnj110  34872  fncvm  35262  iscvm  35264  snmlval  35336  satfv1  35368  satfdm  35374  satffunlem1lem2  35408  satfv0fvfmla0  35418  satfv1fvfmla1  35428  mpstval  35540  fvray  36142  icoreval  37354  fin2solem  37613  fin2so  37614  poimirlem4  37631  cnambfre  37675  istotbnd  37776  isbnd  37787  rngohomval  37971  rngoisoval  37984  idlval  38020  pridlval  38040  maxidlval  38046  lshpset  38979  lflset  39060  pats  39286  llnset  39507  lplnset  39531  lvolset  39574  isline  39741  pmapval  39759  paddval  39800  lhpset  39997  ldilset  40111  ltrnset  40120  dilsetN  40155  trnsetN  40158  diaval  41034  diafn  41036  lpolsetN  41484  lcdvadd  41599  lcdsca  41601  lcdvs  41605  mapdval  41630  mapd1o  41650  unitscyglem5  42200  psrmnd  42555  mhmcopsr  42559  mhmcoaddpsr  42560  rhmcomulpsr  42561  evlselv  42597  mhphf  42607  prjcrvval  42642  isnacs  42715  mzpclval  42736  pell1qrval  42857  pell14qrval  42859  pell1234qrval  42861  elmnc  43148  itgoval  43173  idomodle  43203  idomsubgmo  43205  k0004val  44163  icof  45224  elicores  45546  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  stoweidlem34  46049  fourierdlem2  46124  fourierdlem3  46125  etransclem12  46261  etransclem33  46282  ovnval2b  46567  volicorescl  46568  ovncvrrp  46579  ovnsubaddlem1  46585  ovncvr2  46626  issmflem  46742  smfaddlem1  46778  smfaddlem2  46779  smflimlem1  46786  fvmptrabdm  47305  iccpval  47402  fppr  47713  grtri  47907  assintopval  48121  rngchomrnghmresALTV  48195  bigoval  48470  elbigofrcl  48471  line  48653  rrxline  48655  sphere  48668  rrxsphere  48669