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 3478	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2143  {crab 3416  Vcvv 3455  𝒫 cpw 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564

This theorem is referenced by:  rabex  5309  rabexd  5310  class2set  5325  exse  5621  elfvmptrab1w  7017  elfvmptrab1  7018  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  ovmpt3rabdm  7669  elovmpt3rab1  7670  suppval  8154  mpoxopoveq  8211  wdom2d  9538  scottex  9855  tskwe  9932  fin1a2lem12  10390  hashbclem  14485  wrdnfi  14581  wrd2f1tovbij  14993  hashdvds  16829  hashbcval  17057  brric  20593  psrass1lem  22083  psrcom  22117  dmatval  22649  cpmat  22866  fctop  23161  cctop  23163  ppttop  23164  epttop  23166  cldval  23180  neif  23257  neival  23259  neiptoptop  23288  neiptopnei  23289  ordtbaslem  23345  ordtbas2  23348  ordtopn1  23351  ordtopn2  23352  ordtrest2lem  23360  cmpsublem  23556  kgenval  23692  qtopval  23852  kqfval  23880  ordthmeolem  23958  elmptrab  23984  fbssfi  23994  fgval  24027  flimval  24120  flimfnfcls  24185  ptcmplem2  24210  ptcmplem3  24211  tsmsfbas  24285  eltsms  24290  utopval  24389  blvalps  24542  blval  24543  minveclem3b  25587  minveclem3  25588  minveclem4  25591  cutlt  28125  fusgredgfi  29675  nbgrval  29686  cusgrsize  29804  wwlks  30184  wwlksnextbij  30251  clwwlk  30334  vdn0conngrumgrv2  30547  vdgn1frgrv2  30647  frgrwopreglem1  30663  rabfodom  32851  ordtrest2NEWlem  34312  hasheuni  34475  sigaval  34501  ldgenpisyslem1  34553  ddemeas  34626  braew  34632  imambfm  34652  carsgval  34693  iscvm  35751  cvmsval  35758  fwddifval  36654  fnessref  36868  indexa  38384  supex2g  38388  rfovfvfvd  44729  rfovcnvf1od  44730  fsovfvfvd  44737  fsovcnvlem  44739  cnfex  45748  stoweidlem26  46740  stoweidlem31  46745  stoweidlem34  46748  stoweidlem46  46760  stoweidlem59  46773  salexct  47048  caragenval  47207  clnbgrval  48587  dmatALTbas  49181  lcoop  49191