Theorem rabexg 5274

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3390  Vcvv 3430  𝒫 cpw 4542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  rabex  5276  rabexd  5277  class2set  5292  exse  5584  elfvmptrab1w  6969  elfvmptrab1  6970  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  ovmpt3rabdm  7619  elovmpt3rab1  7620  suppval  8105  mpoxopoveq  8162  wdom2d  9488  scottex  9800  tskwe  9865  fin1a2lem12  10324  hashbclem  14405  wrdnfi  14501  wrd2f1tovbij  14913  hashdvds  16736  hashbcval  16964  brric  20472  psrass1lem  21922  psrcom  21956  dmatval  22467  cpmat  22684  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  cldval  22998  neif  23075  neival  23077  neiptoptop  23106  neiptopnei  23107  ordtbaslem  23163  ordtbas2  23166  ordtopn1  23169  ordtopn2  23170  ordtrest2lem  23178  cmpsublem  23374  kgenval  23510  qtopval  23670  kqfval  23698  ordthmeolem  23776  elmptrab  23802  fbssfi  23812  fgval  23845  flimval  23938  flimfnfcls  24003  ptcmplem2  24028  ptcmplem3  24029  tsmsfbas  24103  eltsms  24108  utopval  24207  blvalps  24360  blval  24361  minveclem3b  25405  minveclem3  25406  minveclem4  25409  cutlt  27938  fusgredgfi  29408  nbgrval  29419  cusgrsize  29538  wwlks  29918  wwlksnextbij  29985  clwwlk  30068  vdn0conngrumgrv2  30281  vdgn1frgrv2  30381  frgrwopreglem1  30397  rabfodom  32590  ordtrest2NEWlem  34082  hasheuni  34245  sigaval  34271  ldgenpisyslem1  34323  ddemeas  34396  braew  34402  imambfm  34422  carsgval  34463  iscvm  35457  cvmsval  35464  fwddifval  36360  fnessref  36555  indexa  38068  supex2g  38072  rfovfvfvd  44448  rfovcnvf1od  44449  fsovfvfvd  44456  fsovcnvlem  44458  cnfex  45477  stoweidlem26  46472  stoweidlem31  46477  stoweidlem34  46480  stoweidlem46  46492  stoweidlem59  46505  salexct  46780  caragenval  46939  clnbgrval  48310  dmatALTbas  48889  lcoop  48899