Theorem rabexg 5292

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3405  Vcvv 3447  𝒫 cpw 4563

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 2701  ax-sep 5251

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  rabex  5294  rabexd  5295  class2set  5310  exse  5598  elfvmptrab1w  6995  elfvmptrab1  6996  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  ovmpt3rabdm  7648  elovmpt3rab1  7649  suppval  8141  mpoxopoveq  8198  wdom2d  9533  scottex  9838  tskwe  9903  fin1a2lem12  10364  hashbclem  14417  wrdnfi  14513  wrd2f1tovbij  14926  hashdvds  16745  hashbcval  16973  brric  20413  psrass1lem  21841  psrcom  21877  dmatval  22379  cpmat  22596  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  cldval  22910  neif  22987  neival  22989  neiptoptop  23018  neiptopnei  23019  ordtbaslem  23075  ordtbas2  23078  ordtopn1  23081  ordtopn2  23082  ordtrest2lem  23090  cmpsublem  23286  kgenval  23422  qtopval  23582  kqfval  23610  ordthmeolem  23688  elmptrab  23714  fbssfi  23724  fgval  23757  flimval  23850  flimfnfcls  23915  ptcmplem2  23940  ptcmplem3  23941  tsmsfbas  24015  eltsms  24020  utopval  24120  blvalps  24273  blval  24274  minveclem3b  25328  minveclem3  25329  minveclem4  25332  cutlt  27840  fusgredgfi  29252  nbgrval  29263  cusgrsize  29382  wwlks  29765  wwlksnextbij  29832  clwwlk  29912  vdn0conngrumgrv2  30125  vdgn1frgrv2  30225  frgrwopreglem1  30241  rabfodom  32434  ordtrest2NEWlem  33912  hasheuni  34075  sigaval  34101  ldgenpisyslem1  34153  ddemeas  34226  braew  34232  imambfm  34253  carsgval  34294  iscvm  35246  cvmsval  35253  fwddifval  36150  fnessref  36345  indexa  37727  supex2g  37731  rfovfvfvd  43992  rfovcnvf1od  43993  fsovfvfvd  44000  fsovcnvlem  44002  cnfex  45022  stoweidlem26  46024  stoweidlem31  46029  stoweidlem34  46032  stoweidlem46  46044  stoweidlem59  46057  salexct  46332  caragenval  46491  clnbgrval  47823  dmatALTbas  48390  lcoop  48400