Theorem rabex 5227

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

Syntax hints:   ∈ wcel 2110  {crab 3142  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951

This theorem is referenced by:  rab2ex  5230  frminex  5529  ssimaex  6742  fvmptrabfv  6793  mptrabex  6982  fnpm  8408  inf3lema  9081  dfac2a  9549  kmlem1  9570  axcc4  9855  axdc3lem2  9867  axdc3lem4  9869  pwfseqlem1  10074  dfuzi  12067  uzval  12239  ixxval  12740  fzval  12888  bitsfval  15766  sadfval  15795  smufval  15820  phicl2  16099  hashgcdeq  16120  prmreclem4  16249  prmreclem5  16250  ismre  16855  fnmre  16856  mrisval  16895  isacs  16916  ismon  16997  isnat  17211  natffn  17213  initoval  17251  termoval  17252  coafval  17318  ismhm  17952  issubm  17962  issubg  18273  isnsg  18301  gimfn  18395  isgim  18396  isga  18415  cntzval  18445  odfval  18654  odngen  18696  gexval  18697  isslw  18727  ablfac1a  19185  ablfac1b  19186  ablfac1c  19187  ablfac1eu  19189  ablfaclem1  19201  ablfaclem2  19202  ablfaclem3  19203  isirred  19443  isrim0  19469  issubrg  19529  issdrg  19568  abvfval  19583  lssset  19699  lmimfn  19792  islmhm  19793  islmim  19828  islbs  19842  rrgval  20054  psrval  20136  psraddcl  20157  psrvscacl  20167  psrgrp  20172  psrlmod  20175  subrgpsr  20193  mvrf  20198  mplsubrg  20214  mplmonmul  20239  mplbas2  20245  opsrval  20249  mhpval  20327  psrplusgpropd  20398  psropprmul  20400  ocvval  20805  elocv  20806  isobs  20858  islinds  20947  scmatval  21107  fncld  21624  cnfval  21835  cnpval  21838  iscnp2  21841  1stcfb  22047  kgenf  22143  xkoopn  22191  dfac14  22220  hmeofn  22359  hmeofval  22360  filunirn  22484  alexsubALTlem2  22650  ucnval  22880  iscfilu  22891  ispsmet  22908  ismet  22927  isxmet  22928  xmetunirn  22941  cncfval  23490  ishtpy  23570  isphtpy  23579  om1bas  23629  cfilfval  23861  caufval  23872  iscmet  23881  dyadmax  24193  vitalilem2  24204  vitalilem3  24205  vitalilem4  24206  itg2monolem1  24345  fncpn  24524  elcpn  24525  mdegleb  24652  mdeg0  24658  mdegaddle  24662  mdegvsca  24664  uc1pval  24727  mon1pval  24729  aannenlem1  24911  aannenlem2  24912  aannenlem3  24913  vmaval  25684  sqff1o  25753  musum  25762  dchrval  25804  dchrbas  25805  tglnfn  26327  tglnunirn  26328  tglngval  26331  israg  26477  iseqlg  26647  ttgitvval  26662  ebtwntg  26762  incistruhgr  26858  usgredgleordALT  27010  vtxdun  27257  vtxdlfgrval  27261  vtxd0nedgb  27264  vtxdushgrfvedglem  27265  vtxdushgrfvedg  27266  vtxdusgr0edgnelALT  27272  1loopgrvd2  27279  usgrvd0nedg  27309  rusgrnumwrdl2  27362  ewlksfval  27377  wwlksn  27609  wspthsn  27620  iswwlksnon  27625  iswspthsnon  27628  wlknwwlksnen  27661  wwlksnexthasheq  27675  rusgrnumwlkg  27750  clwlkclwwlken  27784  clwwlkn  27798  clwwlken  27825  clwlkssizeeq  27858  clwwlknon  27863  clwwlk0on0  27865  konigsberglem5  28029  fusgreg2wsplem  28106  fusgreghash2wsp  28111  2clwwlk  28120  clwwlknonclwlknonen  28136  numclwlk1lem2  28143  numclwwlkovh0  28145  numclwwlkovq  28147  numclwwlkqhash  28148  lnoval  28523  bloval  28552  hmoval  28581  ubthlem1  28641  ubthlem2  28642  ocval  29051  eigvecval  29667  specval  29669  rabfodom  30260  fpwrelmap  30463  mxidlval  30965  ssmxidl  30974  locfinreflem  31099  ordtconnlem1  31162  sigaex  31364  ddemeas  31490  ismbfm  31505  elunirnmbfm  31506  eulerpart  31635  ballotlem8  31789  reprval  31876  bnj110  32125  fncvm  32499  iscvm  32501  snmlval  32573  satfv1  32605  satfdm  32611  satffunlem1lem2  32645  satfv0fvfmla0  32655  satfv1fvfmla1  32665  mpstval  32777  fvray  33597  icoreval  34628  fin2solem  34872  fin2so  34873  poimirlem4  34890  cnambfre  34934  istotbnd  35041  isbnd  35052  rngohomval  35236  rngoisoval  35249  idlval  35285  pridlval  35305  maxidlval  35311  lshpset  36108  lflset  36189  pats  36415  llnset  36635  lplnset  36659  lvolset  36702  isline  36869  pmapval  36887  paddval  36928  lhpset  37125  ldilset  37239  ltrnset  37248  dilsetN  37283  trnsetN  37286  diaval  38162  diafn  38164  lpolsetN  38612  lcdvadd  38727  lcdsca  38729  lcdvs  38733  mapdval  38758  mapd1o  38778  selvval2lem4  39129  isnacs  39294  mzpclval  39315  pell1qrval  39436  pell14qrval  39438  pell1234qrval  39440  elmnc  39729  itgoval  39754  idomodle  39789  idomsubgmo  39791  k0004val  40493  icof  41475  elicores  41802  dvnprodlem1  42224  dvnprodlem2  42225  dvnprodlem3  42226  stoweidlem34  42313  fourierdlem2  42388  fourierdlem3  42389  etransclem12  42525  etransclem33  42546  ovnval2b  42828  volicorescl  42829  ovncvrrp  42840  ovnsubaddlem1  42846  ovncvr2  42887  issmflem  42998  smfaddlem1  43033  smfaddlem2  43034  smflimlem1  43041  fvmptrabdm  43486  iccpval  43569  fppr  43885  ismgmhm  44044  issubmgm  44050  assintopval  44106  rnghmfn  44155  rnghmval  44156  isrngisom  44161  rngchomrnghmresALTV  44261  bigoval  44603  elbigofrcl  44604  line  44713  rrxline  44715  sphere  44728  rrxsphere  44729