Theorem rabexg 5279

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

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3396  Vcvv 3437  𝒫 cpw 4551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915  df-pw 4553

This theorem is referenced by:  rabex  5281  rabexd  5282  class2set  5297  exse  5581  elfvmptrab1w  6965  elfvmptrab1  6966  elovmporab  7601  elovmporab1w  7602  elovmporab1  7603  ovmpt3rabdm  7614  elovmpt3rab1  7615  suppval  8101  mpoxopoveq  8158  wdom2d  9477  scottex  9789  tskwe  9854  fin1a2lem12  10313  hashbclem  14366  wrdnfi  14462  wrd2f1tovbij  14874  hashdvds  16693  hashbcval  16921  brric  20428  psrass1lem  21879  psrcom  21914  dmatval  22427  cpmat  22644  fctop  22939  cctop  22941  ppttop  22942  epttop  22944  cldval  22958  neif  23035  neival  23037  neiptoptop  23066  neiptopnei  23067  ordtbaslem  23123  ordtbas2  23126  ordtopn1  23129  ordtopn2  23130  ordtrest2lem  23138  cmpsublem  23334  kgenval  23470  qtopval  23630  kqfval  23658  ordthmeolem  23736  elmptrab  23762  fbssfi  23772  fgval  23805  flimval  23898  flimfnfcls  23963  ptcmplem2  23988  ptcmplem3  23989  tsmsfbas  24063  eltsms  24068  utopval  24167  blvalps  24320  blval  24321  minveclem3b  25375  minveclem3  25376  minveclem4  25379  cutlt  27896  fusgredgfi  29324  nbgrval  29335  cusgrsize  29454  wwlks  29834  wwlksnextbij  29901  clwwlk  29984  vdn0conngrumgrv2  30197  vdgn1frgrv2  30297  frgrwopreglem1  30313  rabfodom  32506  ordtrest2NEWlem  34007  hasheuni  34170  sigaval  34196  ldgenpisyslem1  34248  ddemeas  34321  braew  34327  imambfm  34347  carsgval  34388  iscvm  35375  cvmsval  35382  fwddifval  36278  fnessref  36473  indexa  37846  supex2g  37850  rfovfvfvd  44160  rfovcnvf1od  44161  fsovfvfvd  44168  fsovcnvlem  44170  cnfex  45189  stoweidlem26  46186  stoweidlem31  46191  stoweidlem34  46194  stoweidlem46  46206  stoweidlem59  46219  salexct  46494  caragenval  46653  clnbgrval  47984  dmatALTbas  48563  lcoop  48573