Theorem rabexg 5277

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

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3396  Vcvv 3437  𝒫 cpw 4549

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 2705  ax-sep 5236

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915  df-pw 4551

This theorem is referenced by:  rabex  5279  rabexd  5280  class2set  5295  exse  5579  elfvmptrab1w  6962  elfvmptrab1  6963  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  ovmpt3rabdm  7611  elovmpt3rab1  7612  suppval  8098  mpoxopoveq  8155  wdom2d  9473  scottex  9785  tskwe  9850  fin1a2lem12  10309  hashbclem  14361  wrdnfi  14457  wrd2f1tovbij  14869  hashdvds  16688  hashbcval  16916  brric  20421  psrass1lem  21871  psrcom  21906  dmatval  22408  cpmat  22625  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  cldval  22939  neif  23016  neival  23018  neiptoptop  23047  neiptopnei  23048  ordtbaslem  23104  ordtbas2  23107  ordtopn1  23110  ordtopn2  23111  ordtrest2lem  23119  cmpsublem  23315  kgenval  23451  qtopval  23611  kqfval  23639  ordthmeolem  23717  elmptrab  23743  fbssfi  23753  fgval  23786  flimval  23879  flimfnfcls  23944  ptcmplem2  23969  ptcmplem3  23970  tsmsfbas  24044  eltsms  24049  utopval  24148  blvalps  24301  blval  24302  minveclem3b  25356  minveclem3  25357  minveclem4  25360  cutlt  27877  fusgredgfi  29305  nbgrval  29316  cusgrsize  29435  wwlks  29815  wwlksnextbij  29882  clwwlk  29965  vdn0conngrumgrv2  30178  vdgn1frgrv2  30278  frgrwopreglem1  30294  rabfodom  32487  ordtrest2NEWlem  33956  hasheuni  34119  sigaval  34145  ldgenpisyslem1  34197  ddemeas  34270  braew  34276  imambfm  34296  carsgval  34337  iscvm  35324  cvmsval  35331  fwddifval  36227  fnessref  36422  indexa  37793  supex2g  37797  rfovfvfvd  44120  rfovcnvf1od  44121  fsovfvfvd  44128  fsovcnvlem  44130  cnfex  45149  stoweidlem26  46148  stoweidlem31  46153  stoweidlem34  46156  stoweidlem46  46168  stoweidlem59  46181  salexct  46456  caragenval  46615  clnbgrval  47946  dmatALTbas  48526  lcoop  48536