Theorem rabex 5235

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

Syntax hints:   ∈ wcel 2114  {crab 3142  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  rab2ex  5238  frminex  5535  ssimaex  6748  fvmptrabfv  6799  mptrabex  6988  fnpm  8414  inf3lema  9087  dfac2a  9555  kmlem1  9576  axcc4  9861  axdc3lem2  9873  axdc3lem4  9875  pwfseqlem1  10080  dfuzi  12074  uzval  12246  ixxval  12747  fzval  12895  bitsfval  15772  sadfval  15801  smufval  15826  phicl2  16105  hashgcdeq  16126  prmreclem4  16255  prmreclem5  16256  ismre  16861  fnmre  16862  mrisval  16901  isacs  16922  ismon  17003  isnat  17217  natffn  17219  initoval  17257  termoval  17258  coafval  17324  ismhm  17958  issubm  17968  issubg  18279  isnsg  18307  gimfn  18401  isgim  18402  isga  18421  cntzval  18451  odfval  18660  odngen  18702  gexval  18703  isslw  18733  ablfac1a  19191  ablfac1b  19192  ablfac1c  19193  ablfac1eu  19195  ablfaclem1  19207  ablfaclem2  19208  ablfaclem3  19209  isirred  19449  isrim0  19475  issubrg  19535  issdrg  19574  abvfval  19589  lssset  19705  lmimfn  19798  islmhm  19799  islmim  19834  islbs  19848  rrgval  20060  psrval  20142  psraddcl  20163  psrvscacl  20173  psrgrp  20178  psrlmod  20181  subrgpsr  20199  mvrf  20204  mplsubrg  20220  mplmonmul  20245  mplbas2  20251  opsrval  20255  mhpval  20333  psrplusgpropd  20404  psropprmul  20406  ocvval  20811  elocv  20812  isobs  20864  islinds  20953  scmatval  21113  fncld  21630  cnfval  21841  cnpval  21844  iscnp2  21847  1stcfb  22053  kgenf  22149  xkoopn  22197  dfac14  22226  hmeofn  22365  hmeofval  22366  filunirn  22490  alexsubALTlem2  22656  ucnval  22886  iscfilu  22897  ispsmet  22914  ismet  22933  isxmet  22934  xmetunirn  22947  cncfval  23496  ishtpy  23576  isphtpy  23585  om1bas  23635  cfilfval  23867  caufval  23878  iscmet  23887  dyadmax  24199  vitalilem2  24210  vitalilem3  24211  vitalilem4  24212  itg2monolem1  24351  fncpn  24530  elcpn  24531  mdegleb  24658  mdeg0  24664  mdegaddle  24668  mdegvsca  24670  uc1pval  24733  mon1pval  24735  aannenlem1  24917  aannenlem2  24918  aannenlem3  24919  vmaval  25690  sqff1o  25759  musum  25768  dchrval  25810  dchrbas  25811  tglnfn  26333  tglnunirn  26334  tglngval  26337  israg  26483  iseqlg  26653  ttgitvval  26668  ebtwntg  26768  incistruhgr  26864  usgredgleordALT  27016  vtxdun  27263  vtxdlfgrval  27267  vtxd0nedgb  27270  vtxdushgrfvedglem  27271  vtxdushgrfvedg  27272  vtxdusgr0edgnelALT  27278  1loopgrvd2  27285  usgrvd0nedg  27315  rusgrnumwrdl2  27368  ewlksfval  27383  wwlksn  27615  wspthsn  27626  iswwlksnon  27631  iswspthsnon  27634  wlknwwlksnen  27667  wwlksnexthasheq  27681  rusgrnumwlkg  27756  clwlkclwwlken  27790  clwwlkn  27804  clwwlken  27831  clwlkssizeeq  27864  clwwlknon  27869  clwwlk0on0  27871  konigsberglem5  28035  fusgreg2wsplem  28112  fusgreghash2wsp  28117  2clwwlk  28126  clwwlknonclwlknonen  28142  numclwlk1lem2  28149  numclwwlkovh0  28151  numclwwlkovq  28153  numclwwlkqhash  28154  lnoval  28529  bloval  28558  hmoval  28587  ubthlem1  28647  ubthlem2  28648  ocval  29057  eigvecval  29673  specval  29675  rabfodom  30266  fpwrelmap  30469  mxidlval  30970  ssmxidl  30979  locfinreflem  31104  ordtconnlem1  31167  sigaex  31369  ddemeas  31495  ismbfm  31510  elunirnmbfm  31511  eulerpart  31640  ballotlem8  31794  reprval  31881  bnj110  32130  fncvm  32504  iscvm  32506  snmlval  32578  satfv1  32610  satfdm  32616  satffunlem1lem2  32650  satfv0fvfmla0  32660  satfv1fvfmla1  32670  mpstval  32782  fvray  33602  icoreval  34637  fin2solem  34893  fin2so  34894  poimirlem4  34911  cnambfre  34955  istotbnd  35062  isbnd  35073  rngohomval  35257  rngoisoval  35270  idlval  35306  pridlval  35326  maxidlval  35332  lshpset  36129  lflset  36210  pats  36436  llnset  36656  lplnset  36680  lvolset  36723  isline  36890  pmapval  36908  paddval  36949  lhpset  37146  ldilset  37260  ltrnset  37269  dilsetN  37304  trnsetN  37307  diaval  38183  diafn  38185  lpolsetN  38633  lcdvadd  38748  lcdsca  38750  lcdvs  38754  mapdval  38779  mapd1o  38799  selvval2lem4  39185  isnacs  39350  mzpclval  39371  pell1qrval  39492  pell14qrval  39494  pell1234qrval  39496  elmnc  39785  itgoval  39810  idomodle  39845  idomsubgmo  39847  k0004val  40549  icof  41531  elicores  41858  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  stoweidlem34  42368  fourierdlem2  42443  fourierdlem3  42444  etransclem12  42580  etransclem33  42601  ovnval2b  42883  volicorescl  42884  ovncvrrp  42895  ovnsubaddlem1  42901  ovncvr2  42942  issmflem  43053  smfaddlem1  43088  smfaddlem2  43089  smflimlem1  43096  fvmptrabdm  43541  iccpval  43624  fppr  43940  ismgmhm  44099  issubmgm  44105  assintopval  44161  rnghmfn  44210  rnghmval  44211  isrngisom  44216  rngchomrnghmresALTV  44316  bigoval  44658  elbigofrcl  44659  line  44768  rrxline  44770  sphere  44783  rrxsphere  44784