Theorem rabexg 4919

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

Syntax hints:   → wi 4   ∈ wcel 2103  {crab 3018  Vcvv 3304   ⊆ wss 3680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-in 3687  df-ss 3694

This theorem is referenced by:  rabex  4920  rabexd  4921  class2set  4937  exse  5182  elfvmptrab1  6419  elovmpt2rab  6997  elovmpt2rab1  6998  ovmpt3rabdm  7009  elovmpt3rab1  7010  suppval  7417  mpt2xopoveq  7465  wdom2d  8601  scottex  8861  tskwe  8889  fin1a2lem12  9346  hashbclem  13349  wrdnfi  13445  wrd2f1tovbij  13825  hashdvds  15603  hashbcval  15829  brric  18867  psrass1lem  19500  psrcom  19532  dmatval  20421  cpmat  20637  fctop  20931  cctop  20933  ppttop  20934  epttop  20936  cldval  20950  neif  21027  neival  21029  neiptoptop  21058  neiptopnei  21059  ordtbaslem  21115  ordtbas2  21118  ordtopn1  21121  ordtopn2  21122  ordtrest2lem  21130  cmpsublem  21325  kgenval  21461  qtopval  21621  kqfval  21649  ordthmeolem  21727  elmptrab  21753  fbssfi  21763  fgval  21796  flimval  21889  flimfnfcls  21954  ptcmplem2  21979  ptcmplem3  21980  tsmsfbas  22053  eltsms  22058  utopval  22158  blvalps  22312  blval  22313  minveclem3b  23320  minveclem3  23321  minveclem4  23324  fusgredgfi  26337  nbgrval  26349  cusgrsize  26481  wwlks  26859  wwlksnextbij  26941  clwwlk  27027  vdn0conngrumgrv2  27269  vdgn1frgrv2  27371  frgrwopreglem1  27387  rabfodom  29572  ordtrest2NEWlem  30198  hasheuni  30377  sigaval  30403  ldgenpisyslem1  30456  ddemeas  30529  braew  30535  imambfm  30554  carsgval  30595  iscvm  31469  cvmsval  31476  fwddifval  32496  fnessref  32579  indexa  33760  supex2g  33764  rfovfvfvd  38716  rfovcnvf1od  38717  fsovfvfvd  38724  fsovcnvlem  38726  cnfex  39603  stoweidlem26  40663  stoweidlem31  40668  stoweidlem34  40671  stoweidlem46  40683  stoweidlem59  40696  salexct  40972  caragenval  41130  dmatALTbas  42617  lcoop  42627