Theorem rabexg 5327

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 4075	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		ssexg 5319	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	mpan 689	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3433  Vcvv 3475   ⊆ wss 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5295

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3953  df-ss 3963

This theorem is referenced by:  rabex  5328  rabexd  5329  class2set  5349  exse  5635  elfvmptrab1w  7013  elfvmptrab1  7014  elovmporab  7639  elovmporab1w  7640  elovmporab1  7641  ovmpt3rabdm  7652  elovmpt3rab1  7653  suppval  8135  mpoxopoveq  8191  wdom2d  9562  scottex  9867  tskwe  9932  fin1a2lem12  10393  hashbclem  14398  wrdnfi  14485  wrd2f1tovbij  14898  hashdvds  16695  hashbcval  16922  brric  20261  psrass1lemOLD  21464  psrass1lem  21467  psrcom  21500  dmatval  21963  cpmat  22180  fctop  22476  cctop  22478  ppttop  22479  epttop  22481  cldval  22496  neif  22573  neival  22575  neiptoptop  22604  neiptopnei  22605  ordtbaslem  22661  ordtbas2  22664  ordtopn1  22667  ordtopn2  22668  ordtrest2lem  22676  cmpsublem  22872  kgenval  23008  qtopval  23168  kqfval  23196  ordthmeolem  23274  elmptrab  23300  fbssfi  23310  fgval  23343  flimval  23436  flimfnfcls  23501  ptcmplem2  23526  ptcmplem3  23527  tsmsfbas  23601  eltsms  23606  utopval  23706  blvalps  23860  blval  23861  minveclem3b  24914  minveclem3  24915  minveclem4  24918  cutlt  27386  fusgredgfi  28549  nbgrval  28560  cusgrsize  28678  wwlks  29056  wwlksnextbij  29123  clwwlk  29203  vdn0conngrumgrv2  29416  vdgn1frgrv2  29516  frgrwopreglem1  29532  rabfodom  31708  ordtrest2NEWlem  32833  hasheuni  33014  sigaval  33040  ldgenpisyslem1  33092  ddemeas  33165  braew  33171  imambfm  33192  carsgval  33233  iscvm  34181  cvmsval  34188  fwddifval  35065  fnessref  35147  indexa  36507  supex2g  36511  rfovfvfvd  42625  rfovcnvf1od  42626  fsovfvfvd  42633  fsovcnvlem  42635  cnfex  43583  stoweidlem26  44615  stoweidlem31  44620  stoweidlem34  44623  stoweidlem46  44635  stoweidlem59  44648  salexct  44923  caragenval  45082  dmatALTbas  46922  lcoop  46932