Theorem rabexg 5256

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

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3069  Vcvv 3433   ⊆ wss 3888

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 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  rabex  5257  rabexd  5258  class2set  5277  exse  5553  elfvmptrab1w  6910  elfvmptrab1  6911  elovmporab  7524  elovmporab1w  7525  elovmporab1  7526  ovmpt3rabdm  7537  elovmpt3rab1  7538  suppval  7988  mpoxopoveq  8044  wdom2d  9348  scottex  9652  tskwe  9717  fin1a2lem12  10176  hashbclem  14173  wrdnfi  14260  wrd2f1tovbij  14684  hashdvds  16485  hashbcval  16712  brric  19997  psrass1lemOLD  21152  psrass1lem  21155  psrcom  21187  dmatval  21650  cpmat  21867  fctop  22163  cctop  22165  ppttop  22166  epttop  22168  cldval  22183  neif  22260  neival  22262  neiptoptop  22291  neiptopnei  22292  ordtbaslem  22348  ordtbas2  22351  ordtopn1  22354  ordtopn2  22355  ordtrest2lem  22363  cmpsublem  22559  kgenval  22695  qtopval  22855  kqfval  22883  ordthmeolem  22961  elmptrab  22987  fbssfi  22997  fgval  23030  flimval  23123  flimfnfcls  23188  ptcmplem2  23213  ptcmplem3  23214  tsmsfbas  23288  eltsms  23293  utopval  23393  blvalps  23547  blval  23548  minveclem3b  24601  minveclem3  24602  minveclem4  24605  fusgredgfi  27701  nbgrval  27712  cusgrsize  27830  wwlks  28209  wwlksnextbij  28276  clwwlk  28356  vdn0conngrumgrv2  28569  vdgn1frgrv2  28669  frgrwopreglem1  28685  rabfodom  30860  ordtrest2NEWlem  31881  hasheuni  32062  sigaval  32088  ldgenpisyslem1  32140  ddemeas  32213  braew  32219  imambfm  32238  carsgval  32279  iscvm  33230  cvmsval  33237  fwddifval  34473  fnessref  34555  indexa  35900  supex2g  35904  rfovfvfvd  41618  rfovcnvf1od  41619  fsovfvfvd  41626  fsovcnvlem  41628  cnfex  42578  stoweidlem26  43574  stoweidlem31  43579  stoweidlem34  43582  stoweidlem46  43594  stoweidlem59  43607  salexct  43880  caragenval  44038  dmatALTbas  45753  lcoop  45763