Theorem rabex 5357

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

Syntax hints:   ∈ wcel 2108  {crab 3443  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  rab2ex  5360  frminex  5679  ssimaex  7007  fvmptrabfv  7061  mptrabex  7262  fnpm  8892  inf3lema  9693  dfac2a  10199  kmlem1  10220  axcc4  10508  axdc3lem2  10520  axdc3lem4  10522  pwfseqlem1  10727  dfuzi  12734  uzval  12905  ixxval  13415  fzval  13569  bitsfval  16469  sadfval  16498  smufval  16523  phicl2  16815  hashgcdeq  16836  prmreclem4  16966  prmreclem5  16967  ismre  17648  fnmre  17649  mrisval  17688  isacs  17709  ismon  17794  isnat  18015  natffn  18017  initofn  18054  termofn  18055  initoval  18060  termoval  18061  coafval  18131  ismgmhm  18734  issubmgm  18740  ismhm  18820  issubm  18838  issubg  19166  isnsg  19195  gimfn  19301  isgim  19302  isga  19331  cntzval  19361  odfval  19574  odngen  19619  gexval  19620  isslw  19650  ablfac1a  20113  ablfac1b  20114  ablfac1c  20115  ablfac1eu  20117  ablfaclem1  20129  ablfaclem2  20130  ablfaclem3  20131  isirred  20445  rnghmfn  20465  rnghmval  20466  isrngim  20471  isrim0OLD  20507  isrim0  20509  issubrng  20573  issubrg  20599  rrgval  20719  issdrg  20811  abvfval  20833  lssset  20954  lmimfn  21048  islmhm  21049  islmim  21084  islbs  21098  ocvval  21708  elocv  21709  isobs  21763  islinds  21852  psrval  21958  psraddcl  21981  psraddclOLD  21982  psrvscacl  21994  psrgrp  21999  psrgrpOLD  22000  psrlmod  22003  subrgpsr  22021  mvrf  22028  mplsubrg  22048  mplmonmul  22077  mplbas2  22083  opsrval  22087  mhpval  22166  mhpmulcl  22176  mhpinvcl  22179  psdcl  22188  psdmplcl  22189  psdadd  22190  psdmul  22193  psrplusgpropd  22258  psropprmul  22260  rhmcomulmpl  22407  scmatval  22531  fncld  23051  cnfval  23262  cnpval  23265  iscnp2  23268  1stcfb  23474  kgenf  23570  xkoopn  23618  dfac14  23647  hmeofn  23786  hmeofval  23787  filunirn  23911  alexsubALTlem2  24077  ucnval  24307  iscfilu  24318  ispsmet  24335  ismet  24354  isxmet  24355  xmetunirn  24368  cncfval  24933  ishtpy  25023  isphtpy  25032  om1bas  25083  cfilfval  25317  caufval  25328  iscmet  25337  dyadmax  25652  vitalilem2  25663  vitalilem3  25664  vitalilem4  25665  itg2monolem1  25805  fncpn  25989  elcpn  25990  mdeg0  26129  mdegaddle  26133  mdegvsca  26135  uc1pval  26199  mon1pval  26201  aannenlem1  26388  aannenlem2  26389  aannenlem3  26390  vmaval  27174  sqff1o  27243  musum  27252  dchrval  27296  dchrbas  27297  leftval  27920  rightval  27921  leftf  27922  rightf  27923  precsexlem4  28252  precsexlem5  28253  tglnfn  28573  tglnunirn  28574  tglngval  28577  israg  28723  iseqlg  28893  ttgitvval  28914  ebtwntg  29015  incistruhgr  29114  usgredgleordALT  29269  vtxdun  29517  vtxdlfgrval  29521  vtxd0nedgb  29524  vtxdushgrfvedglem  29525  vtxdushgrfvedg  29526  vtxdusgr0edgnelALT  29532  1loopgrvd2  29539  usgrvd0nedg  29569  rusgrnumwrdl2  29622  ewlksfval  29637  wwlksn  29870  wspthsn  29881  iswwlksnon  29886  iswspthsnon  29889  wlknwwlksnen  29922  wwlksnexthasheq  29936  rusgrnumwlkg  30010  clwlkclwwlken  30044  clwwlkn  30058  clwwlken  30084  clwlkssizeeq  30117  clwwlknon  30122  clwwlk0on0  30124  konigsberglem5  30288  fusgreg2wsplem  30365  fusgreghash2wsp  30370  2clwwlk  30379  clwwlknonclwlknonen  30395  numclwlk1lem2  30402  numclwwlkovh0  30404  numclwwlkovq  30406  numclwwlkqhash  30407  lnoval  30784  bloval  30813  hmoval  30842  ubthlem1  30902  ubthlem2  30903  ocval  31312  eigvecval  31928  specval  31930  rabfodom  32533  fpwrelmap  32747  nsgmgc  33405  mxidlval  33454  ssmxidl  33467  rprmval  33509  locfinreflem  33786  rspectopn  33813  zarcls1  33815  zarclsun  33816  zarclsiin  33817  zarclsint  33818  zarclssn  33819  zarcls  33820  zartopn  33821  zar0ring  33824  zart0  33825  zarmxt1  33826  zarcmplem  33827  rhmpreimacnlem  33830  rhmpreimacn  33831  ordtconnlem1  33870  sigaex  34074  ddemeas  34200  ismbfm  34215  elunirnmbfm  34216  eulerpart  34347  ballotlem8  34501  reprval  34587  bnj110  34834  fncvm  35225  iscvm  35227  snmlval  35299  satfv1  35331  satfdm  35337  satffunlem1lem2  35371  satfv0fvfmla0  35381  satfv1fvfmla1  35391  mpstval  35503  fvray  36105  icoreval  37319  fin2solem  37566  fin2so  37567  poimirlem4  37584  cnambfre  37628  istotbnd  37729  isbnd  37740  rngohomval  37924  rngoisoval  37937  idlval  37973  pridlval  37993  maxidlval  37999  lshpset  38934  lflset  39015  pats  39241  llnset  39462  lplnset  39486  lvolset  39529  isline  39696  pmapval  39714  paddval  39755  lhpset  39952  ldilset  40066  ltrnset  40075  dilsetN  40110  trnsetN  40113  diaval  40989  diafn  40991  lpolsetN  41439  lcdvadd  41554  lcdsca  41556  lcdvs  41560  mapdval  41585  mapd1o  41605  unitscyglem5  42156  psrmnd  42500  mhmcopsr  42504  mhmcoaddpsr  42505  rhmcomulpsr  42506  evlselv  42542  mhphf  42552  prjcrvval  42587  isnacs  42660  mzpclval  42681  pell1qrval  42802  pell14qrval  42804  pell1234qrval  42806  elmnc  43093  itgoval  43118  idomodle  43152  idomsubgmo  43154  k0004val  44112  icof  45126  elicores  45451  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  stoweidlem34  45955  fourierdlem2  46030  fourierdlem3  46031  etransclem12  46167  etransclem33  46188  ovnval2b  46473  volicorescl  46474  ovncvrrp  46485  ovnsubaddlem1  46491  ovncvr2  46532  issmflem  46648  smfaddlem1  46684  smfaddlem2  46685  smflimlem1  46692  fvmptrabdm  47208  iccpval  47289  fppr  47600  grtri  47791  assintopval  47928  rngchomrnghmresALTV  48002  bigoval  48283  elbigofrcl  48284  line  48466  rrxline  48468  sphere  48481  rrxsphere  48482