Theorem rabexg 5310

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {crab 3418  Vcvv 3457  𝒫 cpw 4564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566

This theorem is used by:  rabex  5311  rabexd  5312  class2set  5327  exse  5623  elfvmptrab1w  7021  elfvmptrab1  7022  elovmporab  7666  elovmporab1w  7667  elovmporab1  7668  ovmpt3rabdm  7679  elovmpt3rab1  7680  suppval  8164  mpoxopoveq  8221  wdom2d  9549  scottex  9869  scottexOLD  9870  tskwe  9952  fin1a2lem12  10410  hashbclem  14507  wrdnfi  14603  wrd2f1tovbij  15021  hashdvds  16856  hashbcval  17084  brric  20643  psrass1lem  22133  psrcom  22167  dmatval  22699  cpmat  22916  fctop  23211  cctop  23213  ppttop  23214  epttop  23216  cldval  23230  neif  23307  neival  23309  neiptoptop  23338  neiptopnei  23339  ordtbaslem  23395  ordtbas2  23398  ordtopn1  23401  ordtopn2  23402  ordtrest2lem  23410  cmpsublem  23606  kgenval  23743  qtopval  23903  kqfval  23931  ordthmeolem  24009  elmptrab  24035  fbssfi  24045  fgval  24078  flimval  24171  flimfnfcls  24236  ptcmplem2  24261  ptcmplem3  24262  tsmsfbas  24336  eltsms  24341  utopval  24440  blvalps  24593  blval  24594  minveclem3b  25638  minveclem3  25639  minveclem4  25642  cutlt  28176  fusgredgfi  29733  nbgrval  29744  cusgrsize  29862  wwlks  30251  wwlksnextbij  30318  clwwlk  30401  vdn0conngrumgrv2  30618  vdgn1frgrv2  30718  frgrwopreglem1  30734  rabfodom  32922  ordtrest2NEWlem  34376  hasheuni  34539  sigaval  34565  ldgenpisyslem1  34618  ddemeas  34691  braew  34697  imambfm  34717  carsgval  34758  iscvm  35788  cvmsval  35795  fwddifval  36691  fnessref  36925  indexa  38442  supex2g  38446  rfovfvfvd  44787  rfovcnvf1od  44788  fsovfvfvd  44795  fsovcnvlem  44797  cnfex  45806  stoweidlem26  46798  stoweidlem31  46803  stoweidlem34  46806  stoweidlem46  46818  stoweidlem59  46831  salexct  47106  caragenval  47265  clnbgrval  48645  dmatALTbas  49238  lcoop  49248