Theorem rabexg 5284

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3401  Vcvv 3442  𝒫 cpw 4556

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 2709  ax-sep 5243

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  rabex  5286  rabexd  5287  class2set  5302  exse  5592  elfvmptrab1w  6977  elfvmptrab1  6978  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  ovmpt3rabdm  7627  elovmpt3rab1  7628  suppval  8114  mpoxopoveq  8171  wdom2d  9497  scottex  9809  tskwe  9874  fin1a2lem12  10333  hashbclem  14387  wrdnfi  14483  wrd2f1tovbij  14895  hashdvds  16714  hashbcval  16942  brric  20449  psrass1lem  21900  psrcom  21935  dmatval  22448  cpmat  22665  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  cldval  22979  neif  23056  neival  23058  neiptoptop  23087  neiptopnei  23088  ordtbaslem  23144  ordtbas2  23147  ordtopn1  23150  ordtopn2  23151  ordtrest2lem  23159  cmpsublem  23355  kgenval  23491  qtopval  23651  kqfval  23679  ordthmeolem  23757  elmptrab  23783  fbssfi  23793  fgval  23826  flimval  23919  flimfnfcls  23984  ptcmplem2  24009  ptcmplem3  24010  tsmsfbas  24084  eltsms  24089  utopval  24188  blvalps  24341  blval  24342  minveclem3b  25396  minveclem3  25397  minveclem4  25400  cutlt  27940  fusgredgfi  29410  nbgrval  29421  cusgrsize  29540  wwlks  29920  wwlksnextbij  29987  clwwlk  30070  vdn0conngrumgrv2  30283  vdgn1frgrv2  30383  frgrwopreglem1  30399  rabfodom  32592  ordtrest2NEWlem  34100  hasheuni  34263  sigaval  34289  ldgenpisyslem1  34341  ddemeas  34414  braew  34420  imambfm  34440  carsgval  34481  iscvm  35475  cvmsval  35482  fwddifval  36378  fnessref  36573  indexa  37984  supex2g  37988  rfovfvfvd  44359  rfovcnvf1od  44360  fsovfvfvd  44367  fsovcnvlem  44369  cnfex  45388  stoweidlem26  46384  stoweidlem31  46389  stoweidlem34  46392  stoweidlem46  46404  stoweidlem59  46417  salexct  46692  caragenval  46851  clnbgrval  48182  dmatALTbas  48761  lcoop  48771