Theorem rabex 5311

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

This proof depends on syntax axioms:   ∈ wcel 2146  {crab 3418  Vcvv 3457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566

This theorem is used by:  rab2ex  5314  frminex  5642  ssimaex  6970  fvmptrabfv  7026  mptrabex  7230  fnpm  8837  inf3lema  9600  dfac2a  10129  kmlem1  10150  axcc4  10438  axdc3lem2  10450  axdc3lem4  10452  pwfseqlem1  10658  dfuzi  12703  uzval  12880  ixxval  13396  fzval  13553  bitsfval  16503  sadfval  16532  smufval  16557  phicl2  16849  hashgcdeq  16871  prmreclem4  17001  prmreclem5  17002  ismre  17664  fnmre  17665  mrisval  17708  isacs  17729  ismon  17812  isnat  18029  natffn  18031  initofn  18066  termofn  18067  initoval  18072  termoval  18073  coafval  18143  ismgmhm  18786  issubmgm  18792  ismhm  18880  issubm  18898  issubg  19236  isnsg  19265  gimfn  19375  isgim  19376  isga  19405  cntzval  19435  odfval  19646  odngen  19691  gexval  19692  isslw  19722  ablfac1a  20185  ablfac1b  20186  ablfac1c  20187  ablfac1eu  20189  ablfaclem1  20201  ablfaclem2  20202  ablfaclem3  20203  isirred  20547  rnghmfn  20567  rnghmval  20568  isrngim  20573  rhmval0  20603  isrim0  20611  rimfn  20635  issubrng  20696  issubrg  20720  rrgval  20846  issdrg  20941  abvfval  20963  lssset  21104  lmimfn  21197  islmhm  21198  islmim  21233  islbs  21247  ocvval  21867  elocv  21868  isobs  21920  islinds  22009  psrval  22115  psraddcl  22139  psrvscacl  22151  psrgrp  22156  psrlmod  22159  subrgpsr  22177  mvrf  22184  mplsubrg  22204  mplmonmul  22237  mplbas2  22243  opsrval  22247  rhmcomulmpl  22325  mhpval  22352  mhpmulcl  22362  mhpinvcl  22365  psdcl  22374  psdmplcl  22375  psdadd  22376  psdmul  22379  psrplusgpropd  22445  psropprmul  22447  scmatval  22711  fncld  23229  cnfval  23440  cnpval  23443  iscnp2  23446  1stcfb  23652  kgenf  23749  xkoopn  23797  dfac14  23826  hmeofn  23965  hmeofval  23966  filunirn  24090  alexsubALTlem2  24256  ucnval  24484  iscfilu  24495  ispsmet  24512  ismet  24531  isxmet  24532  xmetunirn  24545  cncfval  25098  ishtpy  25182  isphtpy  25191  om1bas  25241  cfilfval  25474  caufval  25485  iscmet  25494  dyadmax  25808  vitalilem2  25819  vitalilem3  25820  vitalilem4  25821  itg2monolem1  25960  fncpn  26143  elcpn  26144  mdeg0  26278  mdegaddle  26282  mdegvsca  26284  uc1pval  26348  mon1pval  26350  aannenlem1  26542  aannenlem2  26543  aannenlem3  26544  vmaval  27328  sqff1o  27397  musum  27406  dchrval  27449  dchrbas  27450  leftval  28093  rightval  28094  leftf  28099  rightf  28100  precsexlem4  28454  precsexlem5  28455  tglnfn  28867  tglnunirn  28868  tglngval  28871  israg  29028  tgplnfn  29108  isplng  29111  iseqlg  29239  ttgitvval  29286  ebtwntg  29387  incistruhgr  29484  usgredgleordALT  29642  vtxdun  29889  vtxdlfgrval  29893  vtxd0nedgb  29896  vtxdushgrfvedglem  29897  vtxdushgrfvedg  29898  vtxdusgr0edgnelALT  29904  1loopgrvd2  29911  usgrvd0nedg  29941  rusgrnumwrdl2  29994  ewlksfval  30009  wwlksn  30253  wspthsn  30264  iswwlksnon  30269  iswspthsnon  30272  wlknwwlksnen  30305  wwlksnexthasheq  30319  rusgrnumwlkg  30396  clwlkclwwlken  30430  clwwlkn  30444  clwwlken  30470  clwlkssizeeq  30503  clwwlknon  30508  clwwlk0on0  30510  konigsberglem5  30678  fusgreg2wsplem  30755  fusgreghash2wsp  30760  2clwwlk  30769  clwwlknonclwlknonen  30785  numclwlk1lem2  30792  numclwwlkovh0  30794  numclwwlkovq  30796  numclwwlkqhash  30797  lnoval  31175  bloval  31204  hmoval  31233  ubthlem1  31293  ubthlem2  31294  ocval  31703  eigvecval  32319  specval  32321  rabfodom  32922  fpwrelmap  33148  nsgmgc  33785  mxidlval  33808  ssmxidl  33821  rprmval  33870  selvply1rhmlem4  33977  evlextv  33996  mplvrpmfgalem  33998  mplvrpmga  33999  mplvrpmmhm  34000  mplvrpmrhm  34001  psrmonmul  34004  esplyfval0  34018  esplyfvaln  34028  locfinreflem  34294  rspectopn  34321  zarcls1  34323  zarclsun  34324  zarclsiin  34325  zarclsint  34326  zarclssn  34327  zarcls  34328  zartopn  34329  zar0ring  34332  zart0  34333  zarmxt1  34334  zarcmplem  34335  rhmpreimacnlem  34338  rhmpreimacn  34339  ordtconnlem1  34378  sigaex  34564  ddemeas  34691  ismbfm  34706  elunirnmbfm  34707  eulerpart  34837  ballotlem8  34992  reprval  35062  bnj110  35311  fncvm  35786  iscvm  35788  snmlval  35860  satfv1  35892  satfdm  35898  satffunlem1lem2  35932  satfv0fvfmla0  35942  satfv1fvfmla1  35952  mpstval  36064  fvray  36670  regsfromregtco  37106  icoreval  38056  fin2solem  38314  fin2so  38315  poimirlem4  38332  cnambfre  38376  istotbnd  38478  isbnd  38489  rngohomval  38673  rngoisoval  38686  idlval  38722  pridlval  38742  maxidlval  38748  lshpset  39810  lflset  39891  pats  40117  llnset  40337  lplnset  40361  lvolset  40404  isline  40571  pmapval  40589  paddval  40630  lhpset  40827  ldilset  40941  ltrnset  40950  dilsetN  40985  trnsetN  40988  diaval  41864  diafn  41866  lpolsetN  42314  lcdvadd  42429  lcdsca  42431  lcdvs  42435  mapdval  42460  mapd1o  42480  unitscyglem5  43024  psrmnd  43369  mhmcopsr  43370  mhmcoaddpsr  43371  rhmcomulpsr  43372  evlselv  43379  mhphf  43387  prjcrvval  43422  isnacs  43493  mzpclval  43514  pell1qrval  43631  pell14qrval  43633  pell1234qrval  43635  elmnc  43921  itgoval  43946  idomodle  43976  idomsubgmo  43978  k0004val  44934  permaxsep  45774  icof  45993  elicores  46307  dvnprodlem1  46718  dvnprodlem2  46719  dvnprodlem3  46720  stoweidlem34  46806  fourierdlem2  46881  fourierdlem3  46882  etransclem12  47018  etransclem33  47039  ovnval2b  47324  volicorescl  47325  ovncvrrp  47336  ovnsubaddlem1  47342  ovncvr2  47383  issmflem  47499  smfaddlem1  47535  smfaddlem2  47536  smflimlem1  47543  fvmptrabdm  48088  iccpval  48222  fppr  48549  grtri  48763  assintopval  49027  rngchomrnghmresALTV  49101  bigoval  49386  elbigofrcl  49387  line  49569  rrxline  49571  sphere  49584  rrxsphere  49585