Theorem rabexg 5237

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

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3145  Vcvv 3497   ⊆ wss 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-in 3946  df-ss 3955

This theorem is referenced by:  rabex  5238  rabexd  5239  class2set  5257  exse  5522  elfvmptrab1w  6797  elfvmptrab1  6798  elovmporab  7394  elovmporab1w  7395  elovmporab1  7396  ovmpt3rabdm  7407  elovmpt3rab1  7408  suppval  7835  mpoxopoveq  7888  wdom2d  9047  scottex  9317  tskwe  9382  fin1a2lem12  9836  hashbclem  13813  wrdnfi  13902  wrdnfiOLD  13903  wrd2f1tovbij  14327  hashdvds  16115  hashbcval  16341  brric  19502  psrass1lem  20160  psrcom  20192  dmatval  21104  cpmat  21320  fctop  21615  cctop  21617  ppttop  21618  epttop  21620  cldval  21634  neif  21711  neival  21713  neiptoptop  21742  neiptopnei  21743  ordtbaslem  21799  ordtbas2  21802  ordtopn1  21805  ordtopn2  21806  ordtrest2lem  21814  cmpsublem  22010  kgenval  22146  qtopval  22306  kqfval  22334  ordthmeolem  22412  elmptrab  22438  fbssfi  22448  fgval  22481  flimval  22574  flimfnfcls  22639  ptcmplem2  22664  ptcmplem3  22665  tsmsfbas  22739  eltsms  22744  utopval  22844  blvalps  22998  blval  22999  minveclem3b  24034  minveclem3  24035  minveclem4  24038  fusgredgfi  27110  nbgrval  27121  cusgrsize  27239  wwlks  27616  wwlksnextbij  27683  clwwlk  27764  vdn0conngrumgrv2  27978  vdgn1frgrv2  28078  frgrwopreglem1  28094  rabfodom  30269  ordtrest2NEWlem  31169  hasheuni  31348  sigaval  31374  ldgenpisyslem1  31426  ddemeas  31499  braew  31505  imambfm  31524  carsgval  31565  iscvm  32510  cvmsval  32517  fwddifval  33627  fnessref  33709  indexa  35012  supex2g  35016  rfovfvfvd  40355  rfovcnvf1od  40356  fsovfvfvd  40363  fsovcnvlem  40365  cnfex  41291  stoweidlem26  42318  stoweidlem31  42323  stoweidlem34  42326  stoweidlem46  42338  stoweidlem59  42351  salexct  42624  caragenval  42782  dmatALTbas  44463  lcoop  44473