Theorem rabexg 5332

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

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

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 5300

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 3956  df-ss 3966

This theorem is referenced by:  rabex  5333  rabexd  5334  class2set  5354  exse  5640  elfvmptrab1w  7025  elfvmptrab1  7026  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  ovmpt3rabdm  7665  elovmpt3rab1  7666  suppval  8148  mpoxopoveq  8204  wdom2d  9575  scottex  9880  tskwe  9945  fin1a2lem12  10406  hashbclem  14411  wrdnfi  14498  wrd2f1tovbij  14911  hashdvds  16708  hashbcval  16935  brric  20283  psrass1lemOLD  21493  psrass1lem  21496  psrcom  21529  dmatval  21994  cpmat  22211  fctop  22507  cctop  22509  ppttop  22510  epttop  22512  cldval  22527  neif  22604  neival  22606  neiptoptop  22635  neiptopnei  22636  ordtbaslem  22692  ordtbas2  22695  ordtopn1  22698  ordtopn2  22699  ordtrest2lem  22707  cmpsublem  22903  kgenval  23039  qtopval  23199  kqfval  23227  ordthmeolem  23305  elmptrab  23331  fbssfi  23341  fgval  23374  flimval  23467  flimfnfcls  23532  ptcmplem2  23557  ptcmplem3  23558  tsmsfbas  23632  eltsms  23637  utopval  23737  blvalps  23891  blval  23892  minveclem3b  24945  minveclem3  24946  minveclem4  24949  cutlt  27421  fusgredgfi  28613  nbgrval  28624  cusgrsize  28742  wwlks  29120  wwlksnextbij  29187  clwwlk  29267  vdn0conngrumgrv2  29480  vdgn1frgrv2  29580  frgrwopreglem1  29596  rabfodom  31774  ordtrest2NEWlem  32933  hasheuni  33114  sigaval  33140  ldgenpisyslem1  33192  ddemeas  33265  braew  33271  imambfm  33292  carsgval  33333  iscvm  34281  cvmsval  34288  fwddifval  35165  fnessref  35290  indexa  36649  supex2g  36653  rfovfvfvd  42802  rfovcnvf1od  42803  fsovfvfvd  42810  fsovcnvlem  42812  cnfex  43760  stoweidlem26  44790  stoweidlem31  44795  stoweidlem34  44798  stoweidlem46  44810  stoweidlem59  44823  salexct  45098  caragenval  45257  dmatALTbas  47130  lcoop  47140