Theorem rabexg 5299

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {crab 3413  Vcvv 3451  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rabex  5300  rabexd  5301  class2set  5316  exse  5611  elfvmptrab1w  7019  elfvmptrab1  7020  elovmporab  7665  elovmporab1w  7666  elovmporab1  7667  ovmpt3rabdm  7678  elovmpt3rab1  7679  suppval  8172  mpoxopoveq  8229  wdom2d  9567  scottex  9926  scottexOLD  9927  tskwe  10024  fin1a2lem12  10482  hashbclem  14590  wrdnfi  14686  wrd2f1tovbij  15106  hashdvds  16945  hashbcval  17173  brric  20738  psrass1lem  22234  psrcom  22268  dmatval  22800  cpmat  23020  fctop  23315  cctop  23317  ppttop  23318  epttop  23320  cldval  23334  neif  23411  neival  23413  neiptoptop  23442  neiptopnei  23443  ordtbaslem  23499  ordtbas2  23502  ordtopn1  23505  ordtopn2  23506  ordtrest2lem  23514  cmpsublem  23710  kgenval  23847  qtopval  24007  kqfval  24035  ordthmeolem  24113  elmptrab  24139  fbssfi  24149  fgval  24182  flimval  24275  flimfnfcls  24340  ptcmplem2  24365  ptcmplem3  24366  tsmsfbas  24440  eltsms  24445  utopval  24544  blvalps  24697  blval  24698  minveclem3b  25742  minveclem3  25743  minveclem4  25746  cutlt  28311  fusgredgfi  29899  nbgrval  29910  cusgrsize  30028  wwlks  30417  wwlksnextbij  30484  clwwlk  30567  vdn0conngrumgrv2  30790  vdgn1frgrv2  30890  frgrwopreglem1  30906  rabfodom  33094  ordtrest2NEWlem  34547  hasheuni  34710  sigaval  34736  ldgenpisyslem1  34789  ddemeas  34862  braew  34868  imambfm  34887  carsgval  34928  iscvm  36003  cvmsval  36010  fwddifval  36907  fnessref  37125  indexa  38647  supex2g  38651  rfovfvfvd  44988  rfovcnvf1od  44989  fsovfvfvd  44996  fsovcnvlem  44998  cnfex  46014  stoweidlem26  47005  stoweidlem31  47010  stoweidlem34  47013  stoweidlem46  47025  stoweidlem59  47038  salexct  47313  caragenval  47472  clnbgrval  48889  dmatALTbas  49482  lcoop  49492