Theorem rabexg 5295

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3408  Vcvv 3450  𝒫 cpw 4566

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  rabex  5297  rabexd  5298  class2set  5313  exse  5601  elfvmptrab1w  6998  elfvmptrab1  6999  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  ovmpt3rabdm  7651  elovmpt3rab1  7652  suppval  8144  mpoxopoveq  8201  wdom2d  9540  scottex  9845  tskwe  9910  fin1a2lem12  10371  hashbclem  14424  wrdnfi  14520  wrd2f1tovbij  14933  hashdvds  16752  hashbcval  16980  brric  20420  psrass1lem  21848  psrcom  21884  dmatval  22386  cpmat  22603  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  cldval  22917  neif  22994  neival  22996  neiptoptop  23025  neiptopnei  23026  ordtbaslem  23082  ordtbas2  23085  ordtopn1  23088  ordtopn2  23089  ordtrest2lem  23097  cmpsublem  23293  kgenval  23429  qtopval  23589  kqfval  23617  ordthmeolem  23695  elmptrab  23721  fbssfi  23731  fgval  23764  flimval  23857  flimfnfcls  23922  ptcmplem2  23947  ptcmplem3  23948  tsmsfbas  24022  eltsms  24027  utopval  24127  blvalps  24280  blval  24281  minveclem3b  25335  minveclem3  25336  minveclem4  25339  cutlt  27847  fusgredgfi  29259  nbgrval  29270  cusgrsize  29389  wwlks  29772  wwlksnextbij  29839  clwwlk  29919  vdn0conngrumgrv2  30132  vdgn1frgrv2  30232  frgrwopreglem1  30248  rabfodom  32441  ordtrest2NEWlem  33919  hasheuni  34082  sigaval  34108  ldgenpisyslem1  34160  ddemeas  34233  braew  34239  imambfm  34260  carsgval  34301  iscvm  35253  cvmsval  35260  fwddifval  36157  fnessref  36352  indexa  37734  supex2g  37738  rfovfvfvd  43999  rfovcnvf1od  44000  fsovfvfvd  44007  fsovcnvlem  44009  cnfex  45029  stoweidlem26  46031  stoweidlem31  46036  stoweidlem34  46039  stoweidlem46  46051  stoweidlem59  46064  salexct  46339  caragenval  46498  clnbgrval  47827  dmatALTbas  48394  lcoop  48404