Theorem rabexg 5306

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  {crab 3416  Vcvv 3454  𝒫 cpw 4560

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  rabex  5307  rabexd  5308  class2set  5323  exse  5618  elfvmptrab1w  7052  elfvmptrab1  7053  elovmporab  7699  elovmporab1w  7700  elovmporab1  7701  ovmpt3rabdm  7712  elovmpt3rab1  7713  suppval  8216  mpoxopoveq  8274  wdom2d  9611  scottex  9970  scottexOLD  9971  tskwe  10068  fin1a2lem12  10528  hashbclem  14638  wrdnfi  14734  wrd2f1tovbij  15156  hashdvds  16996  hashbcval  17224  psrass1lem  22296  psrcom  22330  dmatval  22862  cpmat  23082  fctop  23377  cctop  23379  ppttop  23380  epttop  23382  cldval  23396  neif  23473  neival  23475  neiptoptop  23504  neiptopnei  23505  ordtbaslem  23561  ordtbas2  23564  ordtopn1  23567  ordtopn2  23568  ordtrest2lem  23576  cmpsublem  23772  kgenval  23909  qtopval  24069  kqfval  24097  ordthmeolem  24175  elmptrab  24201  fbssfi  24211  fgval  24244  flimval  24337  flimfnfcls  24402  ptcmplem2  24427  ptcmplem3  24428  tsmsfbas  24502  eltsms  24507  utopval  24606  blvalps  24759  blval  24760  minveclem3b  25804  minveclem3  25805  minveclem4  25808  cutlt  28375  fusgredgfi  29963  nbgrval  29974  cusgrsize  30092  wwlks  30481  wwlksnextbij  30548  clwwlk  30631  vdn0conngrumgrv2  30854  vdgn1frgrv2  30954  frgrwopreglem1  30970  rabfodom  33200  ordtrest2NEWlem  34665  hasheuni  34828  sigaval  34854  ldgenpisyslem1  34907  ddemeas  34980  braew  34986  imambfm  35005  omssubadd  35043  carsgval  35046  iscvm  36232  cvmsval  36239  fwddifval  37142  fnessref  37360  indexa  38935  supex2g  38937  rfovfvfvd  45264  rfovcnvf1od  45265  fsovfvfvd  45272  fsovcnvlem  45274  cnfex  46319  stoweidlem26  47309  stoweidlem31  47314  stoweidlem34  47317  stoweidlem46  47329  stoweidlem59  47342  salexct  47617  caragenval  47776  clnbgrval  49193  dmatALTbas  49844  lcoop  49854