Theorem rabexg 5299

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  {crab 3412  Vcvv 3450  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-pw 4558

This theorem is used by:  rabex  5300  rabexd  5301  class2set  5316  exse  5611  elfvmptrab1w  7026  elfvmptrab1  7027  elovmporab  7671  elovmporab1w  7672  elovmporab1  7673  ovmpt3rabdm  7684  elovmpt3rab1  7685  suppval  8185  mpoxopoveq  8243  wdom2d  9581  scottex  9940  scottexOLD  9941  tskwe  10038  fin1a2lem12  10496  hashbclem  14604  wrdnfi  14700  wrd2f1tovbij  15122  hashdvds  16961  hashbcval  17189  psrass1lem  22250  psrcom  22284  dmatval  22816  cpmat  23036  fctop  23331  cctop  23333  ppttop  23334  epttop  23336  cldval  23350  neif  23427  neival  23429  neiptoptop  23458  neiptopnei  23459  ordtbaslem  23515  ordtbas2  23518  ordtopn1  23521  ordtopn2  23522  ordtrest2lem  23530  cmpsublem  23726  kgenval  23863  qtopval  24023  kqfval  24051  ordthmeolem  24129  elmptrab  24155  fbssfi  24165  fgval  24198  flimval  24291  flimfnfcls  24356  ptcmplem2  24381  ptcmplem3  24382  tsmsfbas  24456  eltsms  24461  utopval  24560  blvalps  24713  blval  24714  minveclem3b  25758  minveclem3  25759  minveclem4  25762  cutlt  28327  fusgredgfi  29915  nbgrval  29926  cusgrsize  30044  wwlks  30433  wwlksnextbij  30500  clwwlk  30583  vdn0conngrumgrv2  30806  vdgn1frgrv2  30906  frgrwopreglem1  30922  rabfodom  33152  ordtrest2NEWlem  34604  hasheuni  34767  sigaval  34793  ldgenpisyslem1  34846  ddemeas  34919  braew  34925  imambfm  34944  omssubadd  34982  carsgval  34985  iscvm  36114  cvmsval  36121  fwddifval  37023  fnessref  37241  indexa  38776  supex2g  38780  rfovfvfvd  45112  rfovcnvf1od  45113  fsovfvfvd  45120  fsovcnvlem  45122  cnfex  46153  stoweidlem26  47144  stoweidlem31  47149  stoweidlem34  47152  stoweidlem46  47164  stoweidlem59  47177  salexct  47452  caragenval  47611  clnbgrval  49028  dmatALTbas  49621  lcoop  49631