Theorem rabexg 5276

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3394  Vcvv 3436  𝒫 cpw 4551

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553

This theorem is referenced by:  rabex  5278  rabexd  5279  class2set  5294  exse  5579  elfvmptrab1w  6957  elfvmptrab1  6958  elovmporab  7595  elovmporab1w  7596  elovmporab1  7597  ovmpt3rabdm  7608  elovmpt3rab1  7609  suppval  8095  mpoxopoveq  8152  wdom2d  9472  scottex  9781  tskwe  9846  fin1a2lem12  10305  hashbclem  14359  wrdnfi  14455  wrd2f1tovbij  14867  hashdvds  16686  hashbcval  16914  brric  20389  psrass1lem  21839  psrcom  21875  dmatval  22377  cpmat  22594  fctop  22889  cctop  22891  ppttop  22892  epttop  22894  cldval  22908  neif  22985  neival  22987  neiptoptop  23016  neiptopnei  23017  ordtbaslem  23073  ordtbas2  23076  ordtopn1  23079  ordtopn2  23080  ordtrest2lem  23088  cmpsublem  23284  kgenval  23420  qtopval  23580  kqfval  23608  ordthmeolem  23686  elmptrab  23712  fbssfi  23722  fgval  23755  flimval  23848  flimfnfcls  23913  ptcmplem2  23938  ptcmplem3  23939  tsmsfbas  24013  eltsms  24018  utopval  24118  blvalps  24271  blval  24272  minveclem3b  25326  minveclem3  25327  minveclem4  25330  cutlt  27845  fusgredgfi  29270  nbgrval  29281  cusgrsize  29400  wwlks  29780  wwlksnextbij  29847  clwwlk  29927  vdn0conngrumgrv2  30140  vdgn1frgrv2  30240  frgrwopreglem1  30256  rabfodom  32449  ordtrest2NEWlem  33889  hasheuni  34052  sigaval  34078  ldgenpisyslem1  34130  ddemeas  34203  braew  34209  imambfm  34230  carsgval  34271  iscvm  35232  cvmsval  35239  fwddifval  36136  fnessref  36331  indexa  37713  supex2g  37717  rfovfvfvd  43976  rfovcnvf1od  43977  fsovfvfvd  43984  fsovcnvlem  43986  cnfex  45006  stoweidlem26  46007  stoweidlem31  46012  stoweidlem34  46015  stoweidlem46  46027  stoweidlem59  46040  salexct  46315  caragenval  46474  clnbgrval  47806  dmatALTbas  48386  lcoop  48396