Theorem rabexg 5307

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3415  Vcvv 3459  𝒫 cpw 4575

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 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  rabex  5309  rabexd  5310  class2set  5325  exse  5614  elfvmptrab1w  7012  elfvmptrab1  7013  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  ovmpt3rabdm  7664  elovmpt3rab1  7665  suppval  8159  mpoxopoveq  8216  wdom2d  9592  scottex  9897  tskwe  9962  fin1a2lem12  10423  hashbclem  14468  wrdnfi  14564  wrd2f1tovbij  14977  hashdvds  16792  hashbcval  17020  brric  20462  psrass1lem  21890  psrcom  21926  dmatval  22428  cpmat  22645  fctop  22940  cctop  22942  ppttop  22943  epttop  22945  cldval  22959  neif  23036  neival  23038  neiptoptop  23067  neiptopnei  23068  ordtbaslem  23124  ordtbas2  23127  ordtopn1  23130  ordtopn2  23131  ordtrest2lem  23139  cmpsublem  23335  kgenval  23471  qtopval  23631  kqfval  23659  ordthmeolem  23737  elmptrab  23763  fbssfi  23773  fgval  23806  flimval  23899  flimfnfcls  23964  ptcmplem2  23989  ptcmplem3  23990  tsmsfbas  24064  eltsms  24069  utopval  24169  blvalps  24322  blval  24323  minveclem3b  25378  minveclem3  25379  minveclem4  25382  cutlt  27883  fusgredgfi  29250  nbgrval  29261  cusgrsize  29380  wwlks  29763  wwlksnextbij  29830  clwwlk  29910  vdn0conngrumgrv2  30123  vdgn1frgrv2  30223  frgrwopreglem1  30239  rabfodom  32432  ordtrest2NEWlem  33899  hasheuni  34062  sigaval  34088  ldgenpisyslem1  34140  ddemeas  34213  braew  34219  imambfm  34240  carsgval  34281  iscvm  35227  cvmsval  35234  fwddifval  36126  fnessref  36321  indexa  37703  supex2g  37707  rfovfvfvd  43974  rfovcnvf1od  43975  fsovfvfvd  43982  fsovcnvlem  43984  cnfex  45000  stoweidlem26  46003  stoweidlem31  46008  stoweidlem34  46011  stoweidlem46  46023  stoweidlem59  46036  salexct  46311  caragenval  46470  clnbgrval  47784  dmatALTbas  48325  lcoop  48335