Theorem rabexg 5282

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 5281	. 2 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ 𝒫 𝐴)
2	1	elexd 3464	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3399  Vcvv 3440  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  rabex  5284  rabexd  5285  class2set  5300  exse  5584  elfvmptrab1w  6968  elfvmptrab1  6969  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ovmpt3rabdm  7617  elovmpt3rab1  7618  suppval  8104  mpoxopoveq  8161  wdom2d  9485  scottex  9797  tskwe  9862  fin1a2lem12  10321  hashbclem  14375  wrdnfi  14471  wrd2f1tovbij  14883  hashdvds  16702  hashbcval  16930  brric  20437  psrass1lem  21888  psrcom  21923  dmatval  22436  cpmat  22653  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  cldval  22967  neif  23044  neival  23046  neiptoptop  23075  neiptopnei  23076  ordtbaslem  23132  ordtbas2  23135  ordtopn1  23138  ordtopn2  23139  ordtrest2lem  23147  cmpsublem  23343  kgenval  23479  qtopval  23639  kqfval  23667  ordthmeolem  23745  elmptrab  23771  fbssfi  23781  fgval  23814  flimval  23907  flimfnfcls  23972  ptcmplem2  23997  ptcmplem3  23998  tsmsfbas  24072  eltsms  24077  utopval  24176  blvalps  24329  blval  24330  minveclem3b  25384  minveclem3  25385  minveclem4  25388  cutlt  27928  fusgredgfi  29398  nbgrval  29409  cusgrsize  29528  wwlks  29908  wwlksnextbij  29975  clwwlk  30058  vdn0conngrumgrv2  30271  vdgn1frgrv2  30371  frgrwopreglem1  30387  rabfodom  32580  ordtrest2NEWlem  34079  hasheuni  34242  sigaval  34268  ldgenpisyslem1  34320  ddemeas  34393  braew  34399  imambfm  34419  carsgval  34460  iscvm  35453  cvmsval  35460  fwddifval  36356  fnessref  36551  indexa  37934  supex2g  37938  rfovfvfvd  44244  rfovcnvf1od  44245  fsovfvfvd  44252  fsovcnvlem  44254  cnfex  45273  stoweidlem26  46270  stoweidlem31  46275  stoweidlem34  46278  stoweidlem46  46290  stoweidlem59  46303  salexct  46578  caragenval  46737  clnbgrval  48068  dmatALTbas  48647  lcoop  48657