Theorem rabexg 5355

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3443  Vcvv 3488  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  rabex  5357  rabexd  5358  class2set  5373  exse  5660  elfvmptrab1w  7056  elfvmptrab1  7057  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  ovmpt3rabdm  7709  elovmpt3rab1  7710  suppval  8203  mpoxopoveq  8260  wdom2d  9649  scottex  9954  tskwe  10019  fin1a2lem12  10480  hashbclem  14501  wrdnfi  14596  wrd2f1tovbij  15009  hashdvds  16822  hashbcval  17049  brric  20530  psrass1lem  21975  psrcom  22011  dmatval  22519  cpmat  22736  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  cldval  23052  neif  23129  neival  23131  neiptoptop  23160  neiptopnei  23161  ordtbaslem  23217  ordtbas2  23220  ordtopn1  23223  ordtopn2  23224  ordtrest2lem  23232  cmpsublem  23428  kgenval  23564  qtopval  23724  kqfval  23752  ordthmeolem  23830  elmptrab  23856  fbssfi  23866  fgval  23899  flimval  23992  flimfnfcls  24057  ptcmplem2  24082  ptcmplem3  24083  tsmsfbas  24157  eltsms  24162  utopval  24262  blvalps  24416  blval  24417  minveclem3b  25481  minveclem3  25482  minveclem4  25485  cutlt  27984  fusgredgfi  29360  nbgrval  29371  cusgrsize  29490  wwlks  29868  wwlksnextbij  29935  clwwlk  30015  vdn0conngrumgrv2  30228  vdgn1frgrv2  30328  frgrwopreglem1  30344  rabfodom  32533  ordtrest2NEWlem  33868  hasheuni  34049  sigaval  34075  ldgenpisyslem1  34127  ddemeas  34200  braew  34206  imambfm  34227  carsgval  34268  iscvm  35227  cvmsval  35234  fwddifval  36126  fnessref  36323  indexa  37693  supex2g  37697  rfovfvfvd  43965  rfovcnvf1od  43966  fsovfvfvd  43973  fsovcnvlem  43975  cnfex  44928  stoweidlem26  45947  stoweidlem31  45952  stoweidlem34  45955  stoweidlem46  45967  stoweidlem59  45980  salexct  46255  caragenval  46414  clnbgrval  47696  dmatALTbas  48130  lcoop  48140