Theorem rabexg 5311

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {crab 3419  Vcvv 3458  𝒫 cpw 4565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-in 3915  df-ss 3925  df-pw 4567

This theorem is used by:  rabex  5312  rabexd  5313  class2set  5328  exse  5624  elfvmptrab1w  7021  elfvmptrab1  7022  elovmporab  7662  elovmporab1w  7663  elovmporab1  7664  ovmpt3rabdm  7675  elovmpt3rab1  7676  suppval  8160  mpoxopoveq  8217  wdom2d  9544  scottex  9864  scottexOLD  9865  tskwe  9947  fin1a2lem12  10405  hashbclem  14500  wrdnfi  14596  wrd2f1tovbij  15008  hashdvds  16844  hashbcval  17072  brric  20608  psrass1lem  22098  psrcom  22132  dmatval  22664  cpmat  22881  fctop  23176  cctop  23178  ppttop  23179  epttop  23181  cldval  23195  neif  23272  neival  23274  neiptoptop  23303  neiptopnei  23304  ordtbaslem  23360  ordtbas2  23363  ordtopn1  23366  ordtopn2  23367  ordtrest2lem  23375  cmpsublem  23571  kgenval  23707  qtopval  23867  kqfval  23895  ordthmeolem  23973  elmptrab  23999  fbssfi  24009  fgval  24042  flimval  24135  flimfnfcls  24200  ptcmplem2  24225  ptcmplem3  24226  tsmsfbas  24300  eltsms  24305  utopval  24404  blvalps  24557  blval  24558  minveclem3b  25602  minveclem3  25603  minveclem4  25606  cutlt  28140  fusgredgfi  29690  nbgrval  29701  cusgrsize  29819  wwlks  30199  wwlksnextbij  30266  clwwlk  30349  vdn0conngrumgrv2  30562  vdgn1frgrv2  30662  frgrwopreglem1  30678  rabfodom  32866  ordtrest2NEWlem  34325  hasheuni  34488  sigaval  34514  ldgenpisyslem1  34566  ddemeas  34639  braew  34645  imambfm  34665  carsgval  34706  iscvm  35763  cvmsval  35770  fwddifval  36666  fnessref  36900  indexa  38416  supex2g  38420  rfovfvfvd  44761  rfovcnvf1od  44762  fsovfvfvd  44769  fsovcnvlem  44771  cnfex  45780  stoweidlem26  46772  stoweidlem31  46777  stoweidlem34  46780  stoweidlem46  46792  stoweidlem59  46805  salexct  47080  caragenval  47239  clnbgrval  48619  dmatALTbas  49213  lcoop  49223