Theorem rabexg 5250

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 4009	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		ssexg 5242	. 2 ⊢ (({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
3	1, 2	mpan 686	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3067  Vcvv 3422   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rabex  5251  rabexd  5252  class2set  5271  exse  5543  elfvmptrab1w  6883  elfvmptrab1  6884  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  ovmpt3rabdm  7506  elovmpt3rab1  7507  suppval  7950  mpoxopoveq  8006  wdom2d  9269  scottex  9574  tskwe  9639  fin1a2lem12  10098  hashbclem  14092  wrdnfi  14179  wrd2f1tovbij  14603  hashdvds  16404  hashbcval  16631  brric  19903  psrass1lemOLD  21053  psrass1lem  21056  psrcom  21088  dmatval  21549  cpmat  21766  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  cldval  22082  neif  22159  neival  22161  neiptoptop  22190  neiptopnei  22191  ordtbaslem  22247  ordtbas2  22250  ordtopn1  22253  ordtopn2  22254  ordtrest2lem  22262  cmpsublem  22458  kgenval  22594  qtopval  22754  kqfval  22782  ordthmeolem  22860  elmptrab  22886  fbssfi  22896  fgval  22929  flimval  23022  flimfnfcls  23087  ptcmplem2  23112  ptcmplem3  23113  tsmsfbas  23187  eltsms  23192  utopval  23292  blvalps  23446  blval  23447  minveclem3b  24497  minveclem3  24498  minveclem4  24501  fusgredgfi  27595  nbgrval  27606  cusgrsize  27724  wwlks  28101  wwlksnextbij  28168  clwwlk  28248  vdn0conngrumgrv2  28461  vdgn1frgrv2  28561  frgrwopreglem1  28577  rabfodom  30752  ordtrest2NEWlem  31774  hasheuni  31953  sigaval  31979  ldgenpisyslem1  32031  ddemeas  32104  braew  32110  imambfm  32129  carsgval  32170  iscvm  33121  cvmsval  33128  fwddifval  34391  fnessref  34473  indexa  35818  supex2g  35822  rfovfvfvd  41500  rfovcnvf1od  41501  fsovfvfvd  41508  fsovcnvlem  41510  cnfex  42460  stoweidlem26  43457  stoweidlem31  43462  stoweidlem34  43465  stoweidlem46  43477  stoweidlem59  43490  salexct  43763  caragenval  43921  dmatALTbas  45630  lcoop  45640