Theorem rabexg 5278

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3389  Vcvv 3429  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543

This theorem is referenced by:  rabex  5280  rabexd  5281  class2set  5296  exse  5591  elfvmptrab1w  6975  elfvmptrab1  6976  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  ovmpt3rabdm  7626  elovmpt3rab1  7627  suppval  8112  mpoxopoveq  8169  wdom2d  9495  scottex  9809  tskwe  9874  fin1a2lem12  10333  hashbclem  14414  wrdnfi  14510  wrd2f1tovbij  14922  hashdvds  16745  hashbcval  16973  brric  20481  psrass1lem  21912  psrcom  21946  dmatval  22457  cpmat  22674  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  cldval  22988  neif  23065  neival  23067  neiptoptop  23096  neiptopnei  23097  ordtbaslem  23153  ordtbas2  23156  ordtopn1  23159  ordtopn2  23160  ordtrest2lem  23168  cmpsublem  23364  kgenval  23500  qtopval  23660  kqfval  23688  ordthmeolem  23766  elmptrab  23792  fbssfi  23802  fgval  23835  flimval  23928  flimfnfcls  23993  ptcmplem2  24018  ptcmplem3  24019  tsmsfbas  24093  eltsms  24098  utopval  24197  blvalps  24350  blval  24351  minveclem3b  25395  minveclem3  25396  minveclem4  25399  cutlt  27924  fusgredgfi  29394  nbgrval  29405  cusgrsize  29523  wwlks  29903  wwlksnextbij  29970  clwwlk  30053  vdn0conngrumgrv2  30266  vdgn1frgrv2  30366  frgrwopreglem1  30382  rabfodom  32575  ordtrest2NEWlem  34066  hasheuni  34229  sigaval  34255  ldgenpisyslem1  34307  ddemeas  34380  braew  34386  imambfm  34406  carsgval  34447  iscvm  35441  cvmsval  35448  fwddifval  36344  fnessref  36539  indexa  38054  supex2g  38058  rfovfvfvd  44430  rfovcnvf1od  44431  fsovfvfvd  44438  fsovcnvlem  44440  cnfex  45459  stoweidlem26  46454  stoweidlem31  46459  stoweidlem34  46462  stoweidlem46  46474  stoweidlem59  46487  salexct  46762  caragenval  46921  clnbgrval  48298  dmatALTbas  48877  lcoop  48887