Theorem rabexg 5342

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

Syntax hints:   → wi 4   ∈ wcel 2105  {crab 3432  Vcvv 3477  𝒫 cpw 4604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  rabex  5344  rabexd  5345  class2set  5360  exse  5648  elfvmptrab1w  7042  elfvmptrab1  7043  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  ovmpt3rabdm  7691  elovmpt3rab1  7692  suppval  8185  mpoxopoveq  8242  wdom2d  9617  scottex  9922  tskwe  9987  fin1a2lem12  10448  hashbclem  14487  wrdnfi  14582  wrd2f1tovbij  14995  hashdvds  16808  hashbcval  17035  brric  20520  psrass1lem  21969  psrcom  22005  dmatval  22513  cpmat  22730  fctop  23026  cctop  23028  ppttop  23029  epttop  23031  cldval  23046  neif  23123  neival  23125  neiptoptop  23154  neiptopnei  23155  ordtbaslem  23211  ordtbas2  23214  ordtopn1  23217  ordtopn2  23218  ordtrest2lem  23226  cmpsublem  23422  kgenval  23558  qtopval  23718  kqfval  23746  ordthmeolem  23824  elmptrab  23850  fbssfi  23860  fgval  23893  flimval  23986  flimfnfcls  24051  ptcmplem2  24076  ptcmplem3  24077  tsmsfbas  24151  eltsms  24156  utopval  24256  blvalps  24410  blval  24411  minveclem3b  25475  minveclem3  25476  minveclem4  25479  cutlt  27980  fusgredgfi  29356  nbgrval  29367  cusgrsize  29486  wwlks  29864  wwlksnextbij  29931  clwwlk  30011  vdn0conngrumgrv2  30224  vdgn1frgrv2  30324  frgrwopreglem1  30340  rabfodom  32532  ordtrest2NEWlem  33882  hasheuni  34065  sigaval  34091  ldgenpisyslem1  34143  ddemeas  34216  braew  34222  imambfm  34243  carsgval  34284  iscvm  35243  cvmsval  35250  fwddifval  36143  fnessref  36339  indexa  37719  supex2g  37723  rfovfvfvd  43992  rfovcnvf1od  43993  fsovfvfvd  44000  fsovcnvlem  44002  cnfex  44965  stoweidlem26  45981  stoweidlem31  45986  stoweidlem34  45989  stoweidlem46  46001  stoweidlem59  46014  salexct  46289  caragenval  46448  clnbgrval  47746  dmatALTbas  48246  lcoop  48256