Theorem rabexg 5196

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

Assertion

Ref	Expression
rabexg	⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 3967	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		ssexg 5188	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3057  Vcvv 3397   ⊆ wss 3841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3399  df-in 3848  df-ss 3858

This theorem is referenced by:  rabex  5197  rabexd  5198  class2set  5217  exse  5483  elfvmptrab1w  6795  elfvmptrab1  6796  elovmporab  7401  elovmporab1w  7402  elovmporab1  7403  ovmpt3rabdm  7414  elovmpt3rab1  7415  suppval  7851  mpoxopoveq  7907  wdom2d  9110  scottex  9380  tskwe  9445  fin1a2lem12  9904  hashbclem  13895  wrdnfi  13982  wrd2f1tovbij  14406  hashdvds  16205  hashbcval  16431  brric  19611  psrass1lemOLD  20746  psrass1lem  20749  psrcom  20781  dmatval  21236  cpmat  21453  fctop  21748  cctop  21750  ppttop  21751  epttop  21753  cldval  21767  neif  21844  neival  21846  neiptoptop  21875  neiptopnei  21876  ordtbaslem  21932  ordtbas2  21935  ordtopn1  21938  ordtopn2  21939  ordtrest2lem  21947  cmpsublem  22143  kgenval  22279  qtopval  22439  kqfval  22467  ordthmeolem  22545  elmptrab  22571  fbssfi  22581  fgval  22614  flimval  22707  flimfnfcls  22772  ptcmplem2  22797  ptcmplem3  22798  tsmsfbas  22872  eltsms  22877  utopval  22977  blvalps  23131  blval  23132  minveclem3b  24173  minveclem3  24174  minveclem4  24177  fusgredgfi  27259  nbgrval  27270  cusgrsize  27388  wwlks  27765  wwlksnextbij  27832  clwwlk  27912  vdn0conngrumgrv2  28125  vdgn1frgrv2  28225  frgrwopreglem1  28241  rabfodom  30417  ordtrest2NEWlem  31436  hasheuni  31615  sigaval  31641  ldgenpisyslem1  31693  ddemeas  31766  braew  31772  imambfm  31791  carsgval  31832  iscvm  32784  cvmsval  32791  fwddifval  34094  fnessref  34176  indexa  35503  supex2g  35507  rfovfvfvd  41141  rfovcnvf1od  41142  fsovfvfvd  41149  fsovcnvlem  41151  cnfex  42093  stoweidlem26  43093  stoweidlem31  43098  stoweidlem34  43101  stoweidlem46  43113  stoweidlem59  43126  salexct  43399  caragenval  43557  dmatALTbas  45260  lcoop  45270