Theorem rabexg 5290

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) (Proof shortened by BJ, 24-Jul-2025.)

Assertion

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

Distinct variable group:   𝑥,𝐴

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

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		rabelpw 5289	. 2 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴)
2	1	elexd 3476	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2141  {crab 3413  Vcvv 3453  𝒫 cpw 4552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-in 3909  df-ss 3919  df-pw 4554

This theorem is referenced by:  rabex  5292  rabexd  5293  class2set  5308  exse  5603  elfvmptrab1w  6998  elfvmptrab1  6999  elovmporab  7637  elovmporab1w  7638  elovmporab1  7639  ovmpt3rabdm  7650  elovmpt3rab1  7651  suppval  8136  mpoxopoveq  8193  wdom2d  9522  scottex  9837  tskwe  9902  fin1a2lem12  10362  hashbclem  14459  wrdnfi  14555  wrd2f1tovbij  14967  hashdvds  16801  hashbcval  17029  brric  20540  psrass1lem  21973  psrcom  22007  dmatval  22540  cpmat  22757  fctop  23052  cctop  23054  ppttop  23055  epttop  23057  cldval  23071  neif  23148  neival  23150  neiptoptop  23179  neiptopnei  23180  ordtbaslem  23236  ordtbas2  23239  ordtopn1  23242  ordtopn2  23243  ordtrest2lem  23251  cmpsublem  23447  kgenval  23583  qtopval  23743  kqfval  23771  ordthmeolem  23849  elmptrab  23875  fbssfi  23885  fgval  23918  flimval  24011  flimfnfcls  24076  ptcmplem2  24101  ptcmplem3  24102  tsmsfbas  24176  eltsms  24181  utopval  24280  blvalps  24433  blval  24434  minveclem3b  25478  minveclem3  25479  minveclem4  25482  cutlt  28013  fusgredgfi  29483  nbgrval  29494  cusgrsize  29612  wwlks  29992  wwlksnextbij  30059  clwwlk  30142  vdn0conngrumgrv2  30355  vdgn1frgrv2  30455  frgrwopreglem1  30471  rabfodom  32664  ordtrest2NEWlem  34180  hasheuni  34343  sigaval  34369  ldgenpisyslem1  34421  ddemeas  34494  braew  34500  imambfm  34520  carsgval  34561  iscvm  35570  cvmsval  35577  fwddifval  36473  fnessref  36678  indexa  38193  supex2g  38197  rfovfvfvd  44540  rfovcnvf1od  44541  fsovfvfvd  44548  fsovcnvlem  44550  cnfex  45569  stoweidlem26  46561  stoweidlem31  46566  stoweidlem34  46569  stoweidlem46  46581  stoweidlem59  46594  salexct  46869  caragenval  47028  clnbgrval  48405  dmatALTbas  48984  lcoop  48994