Theorem rabexg 5198

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

Syntax hints:   → wi 4   ∈ wcel 2111  {crab 3110  Vcvv 3441   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  rabex  5199  rabexd  5200  class2set  5219  exse  5483  elfvmptrab1w  6771  elfvmptrab1  6772  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  ovmpt3rabdm  7384  elovmpt3rab1  7385  suppval  7815  mpoxopoveq  7868  wdom2d  9028  scottex  9298  tskwe  9363  fin1a2lem12  9822  hashbclem  13806  wrdnfi  13891  wrd2f1tovbij  14315  hashdvds  16102  hashbcval  16328  brric  19492  psrass1lem  20615  psrcom  20647  dmatval  21097  cpmat  21314  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  cldval  21628  neif  21705  neival  21707  neiptoptop  21736  neiptopnei  21737  ordtbaslem  21793  ordtbas2  21796  ordtopn1  21799  ordtopn2  21800  ordtrest2lem  21808  cmpsublem  22004  kgenval  22140  qtopval  22300  kqfval  22328  ordthmeolem  22406  elmptrab  22432  fbssfi  22442  fgval  22475  flimval  22568  flimfnfcls  22633  ptcmplem2  22658  ptcmplem3  22659  tsmsfbas  22733  eltsms  22738  utopval  22838  blvalps  22992  blval  22993  minveclem3b  24032  minveclem3  24033  minveclem4  24036  fusgredgfi  27115  nbgrval  27126  cusgrsize  27244  wwlks  27621  wwlksnextbij  27688  clwwlk  27768  vdn0conngrumgrv2  27981  vdgn1frgrv2  28081  frgrwopreglem1  28097  rabfodom  30274  ordtrest2NEWlem  31275  hasheuni  31454  sigaval  31480  ldgenpisyslem1  31532  ddemeas  31605  braew  31611  imambfm  31630  carsgval  31671  iscvm  32619  cvmsval  32626  fwddifval  33736  fnessref  33818  indexa  35171  supex2g  35175  rfovfvfvd  40704  rfovcnvf1od  40705  fsovfvfvd  40712  fsovcnvlem  40714  cnfex  41657  stoweidlem26  42668  stoweidlem31  42673  stoweidlem34  42676  stoweidlem46  42688  stoweidlem59  42701  salexct  42974  caragenval  43132  dmatALTbas  44810  lcoop  44820