Theorem rabex 5303

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

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

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rab2ex  5306  frminex  5634  ssimaex  6963  fvmptrabfv  7019  mptrabex  7224  fnpm  8833  inf3lema  9603  dfac2a  10132  kmlem1  10153  axcc4  10441  axdc3lem2  10453  axdc3lem4  10455  pwfseqlem1  10667  dfuzi  12712  uzval  12889  ixxval  13406  fzval  13563  bitsfval  16513  sadfval  16542  smufval  16567  phicl2  16859  hashgcdeq  16881  prmreclem4  17011  prmreclem5  17012  ismre  17674  fnmre  17675  mrisval  17718  isacs  17739  ismon  17822  isnat  18039  natffn  18041  initofn  18076  termofn  18077  initoval  18082  termoval  18083  coafval  18153  ismgmhm  18798  issubmgm  18804  ismhm  18893  issubm  18911  issubg  19249  isnsg  19278  gimfn  19388  isgim  19389  isga  19418  cntzval  19448  odfval  19659  odngen  19704  gexval  19705  isslw  19735  ablfac1a  20198  ablfac1b  20199  ablfac1c  20200  ablfac1eu  20202  ablfaclem1  20214  ablfaclem2  20215  ablfaclem3  20216  isirred  20560  rnghmfn  20580  rnghmval  20581  isrngim  20586  rhmval0  20616  isrim0  20624  rimfn  20648  issubrng  20709  issubrg  20733  rrgval  20859  issdrg  20954  abvfval  20976  lssset  21117  lmimfn  21210  islmhm  21211  islmim  21246  islbs  21260  ocvval  21880  elocv  21881  isobs  21933  islinds  22022  psrval  22130  psraddcl  22154  psrvscacl  22166  psrgrp  22171  psrlmod  22174  subrgpsr  22192  mvrf  22199  mplsubrg  22219  mplmonmul  22252  mplbas2  22258  opsrval  22262  rhmcomulmpl  22340  mhpval  22367  mhpmulcl  22377  mhpinvcl  22380  psdcl  22389  psdmplcl  22390  psdadd  22391  psdmul  22394  psrplusgpropd  22460  psropprmul  22462  scmatval  22726  fncld  23247  cnfval  23458  cnpval  23461  iscnp2  23464  1stcfb  23670  kgenf  23767  xkoopn  23815  dfac14  23844  hmeofn  23983  hmeofval  23984  filunirn  24108  alexsubALTlem2  24274  ucnval  24502  iscfilu  24513  ispsmet  24530  ismet  24549  isxmet  24550  xmetunirn  24563  cncfval  25116  ishtpy  25200  isphtpy  25209  om1bas  25259  cfilfval  25492  caufval  25503  iscmet  25512  dyadmax  25826  vitalilem2  25837  vitalilem3  25838  vitalilem4  25839  itg2monolem1  25978  fncpn  26160  elcpn  26161  mdeg0  26295  mdegaddle  26299  mdegvsca  26301  uc1pval  26365  mon1pval  26367  aannenlem1  26564  aannenlem2  26565  aannenlem3  26566  vmaval  27349  sqff1o  27418  musum  27427  dchrval  27470  dchrbas  27471  leftval  28114  rightval  28115  leftf  28120  rightf  28121  precsexlem4  28475  precsexlem5  28476  tglnfn  28889  tglnunirn  28890  tglngval  28893  israg  29051  tgplnfn  29132  isplng  29135  iseqlg  29291  ttgitvval  29338  ebtwntg  29439  incistruhgr  29536  usgredgleordALT  29694  vtxdun  29941  vtxdlfgrval  29945  vtxd0nedgb  29948  vtxdushgrfvedglem  29949  vtxdushgrfvedg  29950  vtxdusgr0edgnelALT  29956  1loopgrvd2  29963  usgrvd0nedg  29993  rusgrnumwrdl2  30046  ewlksfval  30061  wwlksn  30305  wspthsn  30316  iswwlksnon  30321  iswspthsnon  30324  wlknwwlksnen  30357  wwlksnexthasheq  30371  rusgrnumwlkg  30448  clwlkclwwlken  30482  clwwlkn  30496  clwwlken  30522  clwlkssizeeq  30555  clwwlknon  30560  clwwlk0on0  30562  konigsberglem5  30736  fusgreg2wsplem  30813  fusgreghash2wsp  30818  2clwwlk  30827  clwwlknonclwlknonen  30843  numclwlk1lem2  30850  numclwwlkovh0  30852  numclwwlkovq  30854  numclwwlkqhash  30855  lnoval  31233  bloval  31262  hmoval  31291  ubthlem1  31351  ubthlem2  31352  ocval  31761  eigvecval  32377  specval  32379  rabfodom  32980  fpwrelmap  33204  nsgmgc  33841  mxidlval  33864  ssmxidl  33877  rprmval  33926  selvply1rhmlem4  34033  evlextv  34052  mplvrpmfgalem  34054  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrmonmul  34060  esplyfval0  34074  esplyfvaln  34084  locfinreflem  34350  rspectopn  34377  zarcls1  34379  zarclsun  34380  zarclsiin  34381  zarclsint  34382  zarclssn  34383  zarcls  34384  zartopn  34385  zar0ring  34388  zart0  34389  zarmxt1  34390  zarcmplem  34391  rhmpreimacnlem  34394  rhmpreimacn  34395  ordtconnlem1  34434  sigaex  34620  ddemeas  34747  ismbfm  34762  elunirnmbfm  34763  eulerpart  34893  ballotlem8  35048  reprval  35118  bnj110  35367  fncvm  35836  iscvm  35838  snmlval  35910  satfv1  35942  satfdm  35948  satffunlem1lem2  35982  satfv0fvfmla0  35992  satfv1fvfmla1  36002  mpstval  36114  fvray  36721  regsfromregtco  37157  icoreval  38107  fin2solem  38360  fin2so  38361  poimirlem4  38373  cnambfre  38417  istotbnd  38519  isbnd  38530  rngohomval  38714  rngoisoval  38727  idlval  38763  pridlval  38783  maxidlval  38789  lshpset  39851  lflset  39932  pats  40158  llnset  40378  lplnset  40402  lvolset  40445  isline  40612  pmapval  40630  paddval  40671  lhpset  40868  ldilset  40982  ltrnset  40991  dilsetN  41026  trnsetN  41029  diaval  41905  diafn  41907  lpolsetN  42355  lcdvadd  42470  lcdsca  42472  lcdvs  42476  mapdval  42501  mapd1o  42521  unitscyglem5  43065  psrmnd  43425  mhmcopsr  43426  mhmcoaddpsr  43427  rhmcomulpsr  43428  evlselv  43435  mhphf  43443  prjcrvval  43478  isnacs  43549  mzpclval  43570  pell1qrval  43687  pell14qrval  43689  pell1234qrval  43691  elmnc  43977  itgoval  44002  idomodle  44032  idomsubgmo  44034  k0004val  44990  permaxsep  45830  icof  46049  elicores  46363  dvnprodlem1  46774  dvnprodlem2  46775  dvnprodlem3  46776  stoweidlem34  46862  fourierdlem2  46937  fourierdlem3  46938  etransclem12  47074  etransclem33  47095  ovnval2b  47380  volicorescl  47381  ovncvrrp  47392  ovnsubaddlem1  47398  ovncvr2  47439  issmflem  47555  smfaddlem1  47591  smfaddlem2  47592  smflimlem1  47599  fvmptrabdm  48181  iccpval  48315  fppr  48642  grtri  48856  assintopval  49120  rngchomrnghmresALTV  49194  bigoval  49479  elbigofrcl  49480  line  49662  rrxline  49664  sphere  49677  rrxsphere  49678