Theorem rabexg 5337

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3436  Vcvv 3480  𝒫 cpw 4600

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  rabex  5339  rabexd  5340  class2set  5355  exse  5645  elfvmptrab1w  7043  elfvmptrab1  7044  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  ovmpt3rabdm  7692  elovmpt3rab1  7693  suppval  8187  mpoxopoveq  8244  wdom2d  9620  scottex  9925  tskwe  9990  fin1a2lem12  10451  hashbclem  14491  wrdnfi  14586  wrd2f1tovbij  14999  hashdvds  16812  hashbcval  17040  brric  20504  psrass1lem  21952  psrcom  21988  dmatval  22498  cpmat  22715  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  cldval  23031  neif  23108  neival  23110  neiptoptop  23139  neiptopnei  23140  ordtbaslem  23196  ordtbas2  23199  ordtopn1  23202  ordtopn2  23203  ordtrest2lem  23211  cmpsublem  23407  kgenval  23543  qtopval  23703  kqfval  23731  ordthmeolem  23809  elmptrab  23835  fbssfi  23845  fgval  23878  flimval  23971  flimfnfcls  24036  ptcmplem2  24061  ptcmplem3  24062  tsmsfbas  24136  eltsms  24141  utopval  24241  blvalps  24395  blval  24396  minveclem3b  25462  minveclem3  25463  minveclem4  25466  cutlt  27966  fusgredgfi  29342  nbgrval  29353  cusgrsize  29472  wwlks  29855  wwlksnextbij  29922  clwwlk  30002  vdn0conngrumgrv2  30215  vdgn1frgrv2  30315  frgrwopreglem1  30331  rabfodom  32524  ordtrest2NEWlem  33921  hasheuni  34086  sigaval  34112  ldgenpisyslem1  34164  ddemeas  34237  braew  34243  imambfm  34264  carsgval  34305  iscvm  35264  cvmsval  35271  fwddifval  36163  fnessref  36358  indexa  37740  supex2g  37744  rfovfvfvd  44016  rfovcnvf1od  44017  fsovfvfvd  44024  fsovcnvlem  44026  cnfex  45033  stoweidlem26  46041  stoweidlem31  46046  stoweidlem34  46049  stoweidlem46  46061  stoweidlem59  46074  salexct  46349  caragenval  46508  clnbgrval  47809  dmatALTbas  48318  lcoop  48328