Theorem rabexg 5302

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {crab 3412  Vcvv 3450  𝒫 cpw 4557

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rabex  5303  rabexd  5304  class2set  5319  exse  5615  elfvmptrab1w  7014  elfvmptrab1  7015  elovmporab  7660  elovmporab1w  7661  elovmporab1  7662  ovmpt3rabdm  7673  elovmpt3rab1  7674  suppval  8160  mpoxopoveq  8217  wdom2d  9552  scottex  9872  scottexOLD  9873  tskwe  9955  fin1a2lem12  10413  hashbclem  14517  wrdnfi  14613  wrd2f1tovbij  15033  hashdvds  16866  hashbcval  17094  brric  20656  psrass1lem  22148  psrcom  22182  dmatval  22714  cpmat  22934  fctop  23229  cctop  23231  ppttop  23232  epttop  23234  cldval  23248  neif  23325  neival  23327  neiptoptop  23356  neiptopnei  23357  ordtbaslem  23413  ordtbas2  23416  ordtopn1  23419  ordtopn2  23420  ordtrest2lem  23428  cmpsublem  23624  kgenval  23761  qtopval  23921  kqfval  23949  ordthmeolem  24027  elmptrab  24053  fbssfi  24063  fgval  24096  flimval  24189  flimfnfcls  24254  ptcmplem2  24279  ptcmplem3  24280  tsmsfbas  24354  eltsms  24359  utopval  24458  blvalps  24611  blval  24612  minveclem3b  25656  minveclem3  25657  minveclem4  25660  cutlt  28197  fusgredgfi  29785  nbgrval  29796  cusgrsize  29914  wwlks  30303  wwlksnextbij  30370  clwwlk  30453  vdn0conngrumgrv2  30676  vdgn1frgrv2  30776  frgrwopreglem1  30792  rabfodom  32980  ordtrest2NEWlem  34432  hasheuni  34595  sigaval  34621  ldgenpisyslem1  34674  ddemeas  34747  braew  34753  imambfm  34773  carsgval  34814  iscvm  35838  cvmsval  35845  fwddifval  36742  fnessref  36976  indexa  38483  supex2g  38487  rfovfvfvd  44843  rfovcnvf1od  44844  fsovfvfvd  44851  fsovcnvlem  44853  cnfex  45862  stoweidlem26  46854  stoweidlem31  46859  stoweidlem34  46862  stoweidlem46  46874  stoweidlem59  46887  salexct  47162  caragenval  47321  clnbgrval  48738  dmatALTbas  49331  lcoop  49341