Theorem rabexg 5287

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3402  Vcvv 3444  𝒫 cpw 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  rabex  5289  rabexd  5290  class2set  5305  exse  5591  elfvmptrab1w  6977  elfvmptrab1  6978  elovmporab  7615  elovmporab1w  7616  elovmporab1  7617  ovmpt3rabdm  7628  elovmpt3rab1  7629  suppval  8118  mpoxopoveq  8175  wdom2d  9509  scottex  9814  tskwe  9879  fin1a2lem12  10340  hashbclem  14393  wrdnfi  14489  wrd2f1tovbij  14902  hashdvds  16721  hashbcval  16949  brric  20389  psrass1lem  21817  psrcom  21853  dmatval  22355  cpmat  22572  fctop  22867  cctop  22869  ppttop  22870  epttop  22872  cldval  22886  neif  22963  neival  22965  neiptoptop  22994  neiptopnei  22995  ordtbaslem  23051  ordtbas2  23054  ordtopn1  23057  ordtopn2  23058  ordtrest2lem  23066  cmpsublem  23262  kgenval  23398  qtopval  23558  kqfval  23586  ordthmeolem  23664  elmptrab  23690  fbssfi  23700  fgval  23733  flimval  23826  flimfnfcls  23891  ptcmplem2  23916  ptcmplem3  23917  tsmsfbas  23991  eltsms  23996  utopval  24096  blvalps  24249  blval  24250  minveclem3b  25304  minveclem3  25305  minveclem4  25308  cutlt  27816  fusgredgfi  29228  nbgrval  29239  cusgrsize  29358  wwlks  29738  wwlksnextbij  29805  clwwlk  29885  vdn0conngrumgrv2  30098  vdgn1frgrv2  30198  frgrwopreglem1  30214  rabfodom  32407  ordtrest2NEWlem  33885  hasheuni  34048  sigaval  34074  ldgenpisyslem1  34126  ddemeas  34199  braew  34205  imambfm  34226  carsgval  34267  iscvm  35219  cvmsval  35226  fwddifval  36123  fnessref  36318  indexa  37700  supex2g  37704  rfovfvfvd  43965  rfovcnvf1od  43966  fsovfvfvd  43973  fsovcnvlem  43975  cnfex  44995  stoweidlem26  45997  stoweidlem31  46002  stoweidlem34  46005  stoweidlem46  46017  stoweidlem59  46030  salexct  46305  caragenval  46464  clnbgrval  47796  dmatALTbas  48363  lcoop  48373