Theorem rabexg 5308

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

Syntax hints:   → wi 4   ∈ wcel 2149  {crab 3423  Vcvv 3463  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-pw 4569

This theorem is referenced by:  rabex  5310  rabexd  5311  class2set  5326  exse  5622  elfvmptrab1w  7018  elfvmptrab1  7019  elovmporab  7657  elovmporab1w  7658  elovmporab1  7659  ovmpt3rabdm  7670  elovmpt3rab1  7671  suppval  8157  mpoxopoveq  8214  wdom2d  9541  scottex  9858  tskwe  9935  fin1a2lem12  10394  hashbclem  14488  wrdnfi  14584  wrd2f1tovbij  14996  hashdvds  16833  hashbcval  17061  brric  20585  psrass1lem  22051  psrcom  22085  dmatval  22617  cpmat  22834  fctop  23129  cctop  23131  ppttop  23132  epttop  23134  cldval  23148  neif  23225  neival  23227  neiptoptop  23256  neiptopnei  23257  ordtbaslem  23313  ordtbas2  23316  ordtopn1  23319  ordtopn2  23320  ordtrest2lem  23328  cmpsublem  23524  kgenval  23660  qtopval  23820  kqfval  23848  ordthmeolem  23926  elmptrab  23952  fbssfi  23962  fgval  23995  flimval  24088  flimfnfcls  24153  ptcmplem2  24178  ptcmplem3  24179  tsmsfbas  24253  eltsms  24258  utopval  24357  blvalps  24510  blval  24511  minveclem3b  25555  minveclem3  25556  minveclem4  25559  cutlt  28090  fusgredgfi  29615  nbgrval  29626  cusgrsize  29744  wwlks  30124  wwlksnextbij  30191  clwwlk  30274  vdn0conngrumgrv2  30487  vdgn1frgrv2  30587  frgrwopreglem1  30603  rabfodom  32791  ordtrest2NEWlem  34256  hasheuni  34419  sigaval  34445  ldgenpisyslem1  34497  ddemeas  34570  braew  34576  imambfm  34596  carsgval  34637  iscvm  35649  cvmsval  35656  fwddifval  36552  fnessref  36756  indexa  38271  supex2g  38275  rfovfvfvd  44620  rfovcnvf1od  44621  fsovfvfvd  44628  fsovcnvlem  44630  cnfex  45639  stoweidlem26  46631  stoweidlem31  46636  stoweidlem34  46639  stoweidlem46  46651  stoweidlem59  46664  salexct  46939  caragenval  47098  clnbgrval  48475  dmatALTbas  49065  lcoop  49075