Theorem rabex 5300

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

This proof depends on syntax axioms:   ∈ wcel 2144  {crab 3412  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-pw 4558

This theorem is used by:  rab2ex  5303  frminex  5630  ssimaex  6975  fvmptrabfv  7031  mptrabex  7235  fnpm  8861  inf3lema  9632  dfac2a  10215  kmlem1  10236  axcc4  10524  axdc3lem2  10536  axdc3lem4  10538  pwfseqlem1  10750  dfuzi  12797  uzval  12974  ixxval  13491  fzval  13648  bitsfval  16602  sadfval  16631  smufval  16656  phicl2  16954  hashgcdeq  16976  prmreclem4  17106  prmreclem5  17107  ismre  17769  fnmre  17770  mrisval  17813  isacs  17834  ismon  17917  isnat  18134  natffn  18136  initofn  18171  termofn  18172  initoval  18177  termoval  18178  coafval  18248  ismgmhm  18894  issubmgm  18900  ismhm  18989  issubm  19007  issubg  19345  isnsg  19374  gimfn  19484  isgim  19485  isga  19514  cntzval  19544  odfval  19755  odngen  19800  gexval  19801  isslw  19831  ablfac1a  20294  ablfac1b  20295  ablfac1c  20296  ablfac1eu  20298  ablfaclem1  20310  ablfaclem2  20311  ablfaclem3  20312  isirred  20658  rnghmfn  20678  rnghmval  20679  isrngim  20684  rhmval0  20714  isrim0  20722  rimfn  20746  issubrng  20808  issubrg  20832  rrgval  20958  issdrg  21054  abvfval  21076  lssset  21217  lmimfn  21310  islmhm  21311  islmim  21346  islbs  21360  ocvval  21982  elocv  21983  isobs  22035  islinds  22124  psrval  22232  psraddcl  22256  psrvscacl  22268  psrgrp  22273  psrlmod  22276  subrgpsr  22294  mvrf  22301  mplsubrg  22321  mplmonmul  22354  mplbas2  22360  opsrval  22364  rhmcomulmpl  22442  mhpval  22469  mhpmulcl  22479  mhpinvcl  22482  psdcl  22491  psdmplcl  22492  psdadd  22493  psdmul  22496  psrplusgpropd  22562  psropprmul  22564  scmatval  22828  fncld  23349  cnfval  23560  cnpval  23563  iscnp2  23566  1stcfb  23772  kgenf  23869  xkoopn  23917  dfac14  23946  hmeofn  24085  hmeofval  24086  filunirn  24210  alexsubALTlem2  24376  ucnval  24604  iscfilu  24615  ispsmet  24632  ismet  24651  isxmet  24652  xmetunirn  24665  cncfval  25218  ishtpy  25302  isphtpy  25311  om1bas  25361  cfilfval  25594  caufval  25605  iscmet  25614  dyadmax  25928  vitalilem2  25939  vitalilem3  25940  vitalilem4  25941  itg2monolem1  26080  fncpn  26262  elcpn  26263  mdeg0  26397  mdegaddle  26401  mdegvsca  26403  uc1pval  26467  mon1pval  26469  aannenlem1  26664  aannenlem2  26665  aannenlem3  26666  vmaval  27449  sqff1o  27518  musum  27527  dchrval  27570  dchrbas  27571  leftval  28244  rightval  28245  leftf  28250  rightf  28251  precsexlem4  28605  precsexlem5  28606  tglnfn  29019  tglnunirn  29020  tglngval  29023  israg  29181  tgplnfn  29262  isplng  29265  iseqlg  29421  ttgitvval  29468  ebtwntg  29569  incistruhgr  29666  usgredgleordALT  29824  vtxdun  30071  vtxdlfgrval  30075  vtxd0nedgb  30078  vtxdushgrfvedglem  30079  vtxdushgrfvedg  30080  vtxdusgr0edgnelALT  30086  1loopgrvd2  30093  usgrvd0nedg  30123  rusgrnumwrdl2  30176  ewlksfval  30191  wwlksn  30435  wspthsn  30446  iswwlksnon  30451  iswspthsnon  30454  wlknwwlksnen  30487  wwlksnexthasheq  30501  rusgrnumwlkg  30578  clwlkclwwlken  30612  clwwlkn  30626  clwwlken  30652  clwlkssizeeq  30685  clwwlknon  30690  clwwlk0on0  30692  konigsberglem5  30866  fusgreg2wsplem  30943  fusgreghash2wsp  30948  2clwwlk  30957  clwwlknonclwlknonen  30973  numclwlk1lem2  30980  numclwwlkovh0  30982  numclwwlkovq  30984  numclwwlkqhash  30985  lnoval  31363  bloval  31392  hmoval  31421  ubthlem1  31481  ubthlem2  31482  ocval  31891  eigvecval  32507  specval  32509  rabfodom  33152  fpwrelmap  33375  nsgmgc  34013  mxidlval  34036  ssmxidl  34049  rprmval  34098  selvply1rhmlem4  34205  evlextv  34224  mplvrpmfgalem  34226  mplvrpmga  34227  mplvrpmmhm  34228  mplvrpmrhm  34229  psrmonmul  34232  esplyfval0  34246  esplyfvaln  34256  locfinreflem  34522  rspectopn  34549  zarcls1  34551  zarclsun  34552  zarclsiin  34553  zarclsint  34554  zarclssn  34555  zarcls  34556  zartopn  34557  zar0ring  34560  zart0  34561  zarmxt1  34562  zarcmplem  34563  rhmpreimacnlem  34566  rhmpreimacn  34567  ordtconnlem1  34606  sigaex  34792  ddemeas  34919  ismbfm  34934  elunirnmbfm  34935  eulerpart  35064  ballotlem8  35219  reprval  35289  bnj110  35538  fncvm  36112  iscvm  36114  snmlval  36186  satfv1  36218  satfdm  36224  satffunlem1lem2  36258  satfv0fvfmla0  36268  satfv1fvfmla1  36278  mpstval  36390  fvray  37002  regsfromregtco  37422  icoreval  38385  fin2solem  38638  fin2so  38639  poimirlem4  38651  cnambfre  38695  istotbnd  38812  isbnd  38823  rngohomval  39007  rngoisoval  39020  idlval  39056  pridlval  39076  maxidlval  39082  lshpset  40144  lflset  40225  pats  40451  llnset  40671  lplnset  40695  lvolset  40738  isline  40905  pmapval  40923  paddval  40964  lhpset  41161  ldilset  41275  ltrnset  41284  dilsetN  41319  trnsetN  41322  diaval  42198  diafn  42200  lpolsetN  42648  lcdvadd  42763  lcdsca  42765  lcdvs  42769  mapdval  42794  mapd1o  42814  unitscyglem5  43358  psrmnd  43716  mhmcopsr  43717  mhmcoaddpsr  43718  rhmcomulpsr  43719  evlselv  43726  mhphf  43734  prjcrvval  43777  isnacs  43824  mzpclval  43845  pell1qrval  43962  pell14qrval  43964  pell1234qrval  43966  elmnc  44247  itgoval  44272  idomodle  44302  idomsubgmo  44304  k0004val  45259  permaxsep  46105  icof  46340  elicores  46653  dvnprodlem1  47064  dvnprodlem2  47065  dvnprodlem3  47066  stoweidlem34  47152  fourierdlem2  47227  fourierdlem3  47228  etransclem12  47364  etransclem33  47385  ovnval2b  47670  volicorescl  47671  ovncvrrp  47682  ovnsubaddlem1  47688  ovncvr2  47729  issmflem  47845  smfaddlem1  47881  smfaddlem2  47882  smflimlem1  47889  fvmptrabdm  48471  iccpval  48605  fppr  48932  grtri  49146  assintopval  49410  rngchomrnghmresALTV  49484  bigoval  49769  elbigofrcl  49770  line  49953  rrxline  49955  sphere  49967  rrxsphere  49968