Theorem rabexg 5331

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.)

Assertion

Ref	Expression
rabexg	⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem rabexg

Step	Hyp	Ref	Expression
1		ssrab2 4077	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		ssexg 5323	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	mpan 688	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  {crab 3432  Vcvv 3474   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  rabex  5332  rabexd  5333  class2set  5353  exse  5639  elfvmptrab1w  7024  elfvmptrab1  7025  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  ovmpt3rabdm  7664  elovmpt3rab1  7665  suppval  8147  mpoxopoveq  8203  wdom2d  9574  scottex  9879  tskwe  9944  fin1a2lem12  10405  hashbclem  14410  wrdnfi  14497  wrd2f1tovbij  14910  hashdvds  16707  hashbcval  16934  brric  20282  psrass1lemOLD  21492  psrass1lem  21495  psrcom  21528  dmatval  21993  cpmat  22210  fctop  22506  cctop  22508  ppttop  22509  epttop  22511  cldval  22526  neif  22603  neival  22605  neiptoptop  22634  neiptopnei  22635  ordtbaslem  22691  ordtbas2  22694  ordtopn1  22697  ordtopn2  22698  ordtrest2lem  22706  cmpsublem  22902  kgenval  23038  qtopval  23198  kqfval  23226  ordthmeolem  23304  elmptrab  23330  fbssfi  23340  fgval  23373  flimval  23466  flimfnfcls  23531  ptcmplem2  23556  ptcmplem3  23557  tsmsfbas  23631  eltsms  23636  utopval  23736  blvalps  23890  blval  23891  minveclem3b  24944  minveclem3  24945  minveclem4  24948  cutlt  27416  fusgredgfi  28579  nbgrval  28590  cusgrsize  28708  wwlks  29086  wwlksnextbij  29153  clwwlk  29233  vdn0conngrumgrv2  29446  vdgn1frgrv2  29546  frgrwopreglem1  29562  rabfodom  31738  ordtrest2NEWlem  32897  hasheuni  33078  sigaval  33104  ldgenpisyslem1  33156  ddemeas  33229  braew  33235  imambfm  33256  carsgval  33297  iscvm  34245  cvmsval  34252  fwddifval  35129  fnessref  35237  indexa  36596  supex2g  36600  rfovfvfvd  42744  rfovcnvf1od  42745  fsovfvfvd  42752  fsovcnvlem  42754  cnfex  43702  stoweidlem26  44732  stoweidlem31  44737  stoweidlem34  44740  stoweidlem46  44752  stoweidlem59  44765  salexct  45040  caragenval  45199  dmatALTbas  47072  lcoop  47082