Theorem rabex 5278

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

Syntax hints:   ∈ wcel 2109  {crab 3394  Vcvv 3436

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553

This theorem is referenced by:  rab2ex  5281  frminex  5598  ssimaex  6908  fvmptrabfv  6962  mptrabex  7161  fnpm  8761  inf3lema  9520  dfac2a  10024  kmlem1  10045  axcc4  10333  axdc3lem2  10345  axdc3lem4  10347  pwfseqlem1  10552  dfuzi  12567  uzval  12737  ixxval  13256  fzval  13412  bitsfval  16334  sadfval  16363  smufval  16388  phicl2  16679  hashgcdeq  16701  prmreclem4  16831  prmreclem5  16832  ismre  17492  fnmre  17493  mrisval  17536  isacs  17557  ismon  17640  isnat  17857  natffn  17859  initofn  17894  termofn  17895  initoval  17900  termoval  17901  coafval  17971  ismgmhm  18570  issubmgm  18576  ismhm  18659  issubm  18677  issubg  19005  isnsg  19034  gimfn  19140  isgim  19141  isga  19170  cntzval  19200  odfval  19411  odngen  19456  gexval  19457  isslw  19487  ablfac1a  19950  ablfac1b  19951  ablfac1c  19952  ablfac1eu  19954  ablfaclem1  19966  ablfaclem2  19967  ablfaclem3  19968  isirred  20304  rnghmfn  20324  rnghmval  20325  isrngim  20330  isrim0OLD  20366  isrim0  20368  issubrng  20432  issubrg  20456  rrgval  20582  issdrg  20673  abvfval  20695  lssset  20836  lmimfn  20930  islmhm  20931  islmim  20966  islbs  20980  ocvval  21574  elocv  21575  isobs  21627  islinds  21716  psrval  21822  psraddcl  21845  psraddclOLD  21846  psrvscacl  21858  psrgrp  21863  psrgrpOLD  21864  psrlmod  21867  subrgpsr  21885  mvrf  21892  mplsubrg  21912  mplmonmul  21941  mplbas2  21947  opsrval  21951  mhpval  22024  mhpmulcl  22034  mhpinvcl  22037  psdcl  22046  psdmplcl  22047  psdadd  22048  psdmul  22051  psrplusgpropd  22118  psropprmul  22120  rhmcomulmpl  22267  scmatval  22389  fncld  22907  cnfval  23118  cnpval  23121  iscnp2  23124  1stcfb  23330  kgenf  23426  xkoopn  23474  dfac14  23503  hmeofn  23642  hmeofval  23643  filunirn  23767  alexsubALTlem2  23933  ucnval  24162  iscfilu  24173  ispsmet  24190  ismet  24209  isxmet  24210  xmetunirn  24223  cncfval  24779  ishtpy  24869  isphtpy  24878  om1bas  24929  cfilfval  25162  caufval  25173  iscmet  25182  dyadmax  25497  vitalilem2  25508  vitalilem3  25509  vitalilem4  25510  itg2monolem1  25649  fncpn  25833  elcpn  25834  mdeg0  25973  mdegaddle  25977  mdegvsca  25979  uc1pval  26043  mon1pval  26045  aannenlem1  26234  aannenlem2  26235  aannenlem3  26236  vmaval  27021  sqff1o  27090  musum  27099  dchrval  27143  dchrbas  27144  leftval  27773  rightval  27774  leftf  27779  rightf  27780  precsexlem4  28117  precsexlem5  28118  tglnfn  28492  tglnunirn  28493  tglngval  28496  israg  28642  iseqlg  28812  ttgitvval  28827  ebtwntg  28927  incistruhgr  29024  usgredgleordALT  29179  vtxdun  29427  vtxdlfgrval  29431  vtxd0nedgb  29434  vtxdushgrfvedglem  29435  vtxdushgrfvedg  29436  vtxdusgr0edgnelALT  29442  1loopgrvd2  29449  usgrvd0nedg  29479  rusgrnumwrdl2  29532  ewlksfval  29547  wwlksn  29782  wspthsn  29793  iswwlksnon  29798  iswspthsnon  29801  wlknwwlksnen  29834  wwlksnexthasheq  29848  rusgrnumwlkg  29922  clwlkclwwlken  29956  clwwlkn  29970  clwwlken  29996  clwlkssizeeq  30029  clwwlknon  30034  clwwlk0on0  30036  konigsberglem5  30200  fusgreg2wsplem  30277  fusgreghash2wsp  30282  2clwwlk  30291  clwwlknonclwlknonen  30307  numclwlk1lem2  30314  numclwwlkovh0  30316  numclwwlkovq  30318  numclwwlkqhash  30319  lnoval  30696  bloval  30725  hmoval  30754  ubthlem1  30814  ubthlem2  30815  ocval  31224  eigvecval  31840  specval  31842  rabfodom  32449  fpwrelmap  32676  nsgmgc  33349  mxidlval  33398  ssmxidl  33411  rprmval  33453  mplvrpmfgalem  33545  mplvrpmga  33546  locfinreflem  33807  rspectopn  33834  zarcls1  33836  zarclsun  33837  zarclsiin  33838  zarclsint  33839  zarclssn  33840  zarcls  33841  zartopn  33842  zar0ring  33845  zart0  33846  zarmxt1  33847  zarcmplem  33848  rhmpreimacnlem  33851  rhmpreimacn  33852  ordtconnlem1  33891  sigaex  34077  ddemeas  34203  ismbfm  34218  elunirnmbfm  34219  eulerpart  34350  ballotlem8  34505  reprval  34578  bnj110  34825  fncvm  35230  iscvm  35232  snmlval  35304  satfv1  35336  satfdm  35342  satffunlem1lem2  35376  satfv0fvfmla0  35386  satfv1fvfmla1  35396  mpstval  35508  fvray  36115  icoreval  37327  fin2solem  37586  fin2so  37587  poimirlem4  37604  cnambfre  37648  istotbnd  37749  isbnd  37760  rngohomval  37944  rngoisoval  37957  idlval  37993  pridlval  38013  maxidlval  38019  lshpset  38957  lflset  39038  pats  39264  llnset  39484  lplnset  39508  lvolset  39551  isline  39718  pmapval  39736  paddval  39777  lhpset  39974  ldilset  40088  ltrnset  40097  dilsetN  40132  trnsetN  40135  diaval  41011  diafn  41013  lpolsetN  41461  lcdvadd  41576  lcdsca  41578  lcdvs  41582  mapdval  41607  mapd1o  41627  unitscyglem5  42172  psrmnd  42518  mhmcopsr  42522  mhmcoaddpsr  42523  rhmcomulpsr  42524  evlselv  42560  mhphf  42570  prjcrvval  42605  isnacs  42677  mzpclval  42698  pell1qrval  42819  pell14qrval  42821  pell1234qrval  42823  elmnc  43109  itgoval  43134  idomodle  43164  idomsubgmo  43166  k0004val  44123  permaxsep  44981  icof  45197  elicores  45514  dvnprodlem1  45927  dvnprodlem2  45928  dvnprodlem3  45929  stoweidlem34  46015  fourierdlem2  46090  fourierdlem3  46091  etransclem12  46227  etransclem33  46248  ovnval2b  46533  volicorescl  46534  ovncvrrp  46545  ovnsubaddlem1  46551  ovncvr2  46592  issmflem  46708  smfaddlem1  46744  smfaddlem2  46745  smflimlem1  46752  fvmptrabdm  47277  iccpval  47399  fppr  47710  grtri  47924  assintopval  48189  rngchomrnghmresALTV  48263  bigoval  48534  elbigofrcl  48535  line  48717  rrxline  48719  sphere  48732  rrxsphere  48733