Theorem rabexg 5265

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

Syntax hints:   → wi 4   ∈ wcel 2119  {crab 3391  Vcvv 3431  𝒫 cpw 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531

This theorem is referenced by:  rabex  5267  rabexd  5268  class2set  5283  exse  5578  elfvmptrab1w  6963  elfvmptrab1  6964  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  ovmpt3rabdm  7615  elovmpt3rab1  7616  suppval  8102  mpoxopoveq  8159  wdom2d  9485  scottex  9800  tskwe  9865  fin1a2lem12  10324  hashbclem  14405  wrdnfi  14501  wrd2f1tovbij  14913  hashdvds  16736  hashbcval  16964  brric  20475  psrass1lem  21908  psrcom  21942  dmatval  22475  cpmat  22692  fctop  22987  cctop  22989  ppttop  22990  epttop  22992  cldval  23006  neif  23083  neival  23085  neiptoptop  23114  neiptopnei  23115  ordtbaslem  23171  ordtbas2  23174  ordtopn1  23177  ordtopn2  23178  ordtrest2lem  23186  cmpsublem  23382  kgenval  23518  qtopval  23678  kqfval  23706  ordthmeolem  23784  elmptrab  23810  fbssfi  23820  fgval  23853  flimval  23946  flimfnfcls  24011  ptcmplem2  24036  ptcmplem3  24037  tsmsfbas  24111  eltsms  24116  utopval  24215  blvalps  24368  blval  24369  minveclem3b  25413  minveclem3  25414  minveclem4  25417  cutlt  27942  fusgredgfi  29412  nbgrval  29423  cusgrsize  29541  wwlks  29921  wwlksnextbij  29988  clwwlk  30071  vdn0conngrumgrv2  30284  vdgn1frgrv2  30384  frgrwopreglem1  30400  rabfodom  32593  ordtrest2NEWlem  34106  hasheuni  34269  sigaval  34295  ldgenpisyslem1  34347  ddemeas  34420  braew  34426  imambfm  34446  carsgval  34487  iscvm  35487  cvmsval  35494  fwddifval  36390  fnessref  36585  indexa  38100  supex2g  38104  rfovfvfvd  44447  rfovcnvf1od  44448  fsovfvfvd  44455  fsovcnvlem  44457  cnfex  45476  stoweidlem26  46469  stoweidlem31  46474  stoweidlem34  46477  stoweidlem46  46489  stoweidlem59  46502  salexct  46777  caragenval  46936  clnbgrval  48313  dmatALTbas  48892  lcoop  48902