Theorem rabexg 5270

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

Syntax hints:   → wi 4   ∈ wcel 2111  {crab 3395  Vcvv 3436  𝒫 cpw 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4547

This theorem is referenced by:  rabex  5272  rabexd  5273  class2set  5288  exse  5571  elfvmptrab1w  6951  elfvmptrab1  6952  elovmporab  7587  elovmporab1w  7588  elovmporab1  7589  ovmpt3rabdm  7600  elovmpt3rab1  7601  suppval  8087  mpoxopoveq  8144  wdom2d  9461  scottex  9773  tskwe  9838  fin1a2lem12  10297  hashbclem  14354  wrdnfi  14450  wrd2f1tovbij  14862  hashdvds  16681  hashbcval  16909  brric  20414  psrass1lem  21864  psrcom  21900  dmatval  22402  cpmat  22619  fctop  22914  cctop  22916  ppttop  22917  epttop  22919  cldval  22933  neif  23010  neival  23012  neiptoptop  23041  neiptopnei  23042  ordtbaslem  23098  ordtbas2  23101  ordtopn1  23104  ordtopn2  23105  ordtrest2lem  23113  cmpsublem  23309  kgenval  23445  qtopval  23605  kqfval  23633  ordthmeolem  23711  elmptrab  23737  fbssfi  23747  fgval  23780  flimval  23873  flimfnfcls  23938  ptcmplem2  23963  ptcmplem3  23964  tsmsfbas  24038  eltsms  24043  utopval  24142  blvalps  24295  blval  24296  minveclem3b  25350  minveclem3  25351  minveclem4  25354  cutlt  27871  fusgredgfi  29298  nbgrval  29309  cusgrsize  29428  wwlks  29808  wwlksnextbij  29875  clwwlk  29955  vdn0conngrumgrv2  30168  vdgn1frgrv2  30268  frgrwopreglem1  30284  rabfodom  32477  ordtrest2NEWlem  33927  hasheuni  34090  sigaval  34116  ldgenpisyslem1  34168  ddemeas  34241  braew  34247  imambfm  34267  carsgval  34308  iscvm  35295  cvmsval  35302  fwddifval  36196  fnessref  36391  indexa  37773  supex2g  37777  rfovfvfvd  44036  rfovcnvf1od  44037  fsovfvfvd  44044  fsovcnvlem  44046  cnfex  45065  stoweidlem26  46064  stoweidlem31  46069  stoweidlem34  46072  stoweidlem46  46084  stoweidlem59  46097  salexct  46372  caragenval  46531  clnbgrval  47853  dmatALTbas  48433  lcoop  48443