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  27419  fusgredgfi  28582  nbgrval  28593  cusgrsize  28711  wwlks  29089  wwlksnextbij  29156  clwwlk  29236  vdn0conngrumgrv2  29449  vdgn1frgrv2  29549  frgrwopreglem1  29565  rabfodom  31743  ordtrest2NEWlem  32902  hasheuni  33083  sigaval  33109  ldgenpisyslem1  33161  ddemeas  33234  braew  33240  imambfm  33261  carsgval  33302  iscvm  34250  cvmsval  34257  fwddifval  35134  fnessref  35242  indexa  36601  supex2g  36605  rfovfvfvd  42754  rfovcnvf1od  42755  fsovfvfvd  42762  fsovcnvlem  42764  cnfex  43712  stoweidlem26  44742  stoweidlem31  44747  stoweidlem34  44750  stoweidlem46  44762  stoweidlem59  44775  salexct  45050  caragenval  45209  dmatALTbas  47082  lcoop  47092