Theorem rabexg 4812

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)

Assertion

Ref	Expression
rabexg	|- ( A e. V -> { x e. A | ph } e. _V )

Distinct variable group:   x, A

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 3687	. 2 |- { x e. A | ph } C_ A
2		ssexg 4804	. 2 |- ( ( { x e. A | ph } C_ A /\ A e. V ) -> { x e. A | ph } e. _V )
3	1, 2	mpan 706	1 |- ( A e. V -> { x e. A | ph } e. _V )

Syntax hints:   -> wi 4   e. wcel 1990   {crab 2916   _Vcvv 3200   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  rabex  4813  rabexd  4814  class2set  4832  exse  5078  elfvmptrab1  6305  elovmpt2rab  6880  elovmpt2rab1  6881  ovmpt3rabdm  6892  elovmpt3rab1  6893  suppval  7297  mpt2xopoveq  7345  wdom2d  8485  scottex  8748  tskwe  8776  fin1a2lem12  9233  hashbclem  13236  wrdnfi  13338  wrd2f1tovbij  13703  hashdvds  15480  hashbcval  15706  brric  18744  psrass1lem  19377  psrcom  19409  dmatval  20298  cpmat  20514  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  cldval  20827  neif  20904  neival  20906  neiptoptop  20935  neiptopnei  20936  ordtbaslem  20992  ordtbas2  20995  ordtopn1  20998  ordtopn2  20999  ordtrest2lem  21007  cmpsublem  21202  kgenval  21338  qtopval  21498  kqfval  21526  ordthmeolem  21604  elmptrab  21630  fbssfi  21641  fgval  21674  flimval  21767  flimfnfcls  21832  ptcmplem2  21857  ptcmplem3  21858  tsmsfbas  21931  eltsms  21936  utopval  22036  blvalps  22190  blval  22191  minveclem3b  23199  minveclem3  23200  minveclem4  23203  fusgredgfi  26217  nbgrval  26234  cusgrsize  26350  wwlks  26727  wwlksnextbij  26797  clwwlks  26879  vdn0conngrumgrv2  27056  vdgn1frgrv2  27160  frgrwopreglem1  27176  rabfodom  29344  ordtrest2NEWlem  29968  hasheuni  30147  sigaval  30173  ldgenpisyslem1  30226  ddemeas  30299  braew  30305  imambfm  30324  carsgval  30365  iscvm  31241  cvmsval  31248  fwddifval  32269  fnessref  32352  indexa  33528  supex2g  33532  rfovfvfvd  38297  rfovcnvf1od  38298  fsovfvfvd  38305  fsovcnvlem  38307  cnfex  39187  stoweidlem26  40243  stoweidlem31  40248  stoweidlem34  40251  stoweidlem46  40263  stoweidlem59  40276  salexct  40552  caragenval  40707  dmatALTbas  42190  lcoop  42200