Theorem rabexg 4739

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

Syntax hints:   → wi 4   ∈ wcel 1977  {crab 2900  Vcvv 3173   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  rabex  4740  rabexd  4741  class2set  4758  exse  5002  elfvmptrab1  6213  elovmpt2rab  6778  elovmpt2rab1  6779  ovmpt3rabdm  6790  elovmpt3rab1  6791  suppval  7184  mpt2xopoveq  7232  wdom2d  8368  scottex  8631  tskwe  8659  fin1a2lem12  9116  hashbclem  13093  wrdnfi  13193  wrd2f1tovbij  13551  hashdvds  15318  hashbcval  15544  brric  18567  psrass1lem  19198  psrcom  19230  dmatval  20117  cpmat  20333  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  cldval  20637  neif  20714  neival  20716  neiptoptop  20745  neiptopnei  20746  ordtbaslem  20802  ordtbas2  20805  ordtopn1  20808  ordtopn2  20809  ordtrest2lem  20817  cmpsublem  21012  kgenval  21148  qtopval  21308  kqfval  21336  ordthmeolem  21414  elmptrab  21440  fbssfi  21451  fgval  21484  flimval  21577  flimfnfcls  21642  ptcmplem2  21667  ptcmplem3  21668  tsmsfbas  21741  eltsms  21746  utopval  21846  blvalps  22000  blval  22001  minveclem3b  23007  minveclem3  23008  minveclem4  23011  fiusgraedgfi  25936  nbgraop  25952  isuvtx  26016  wwlk  26209  wwlkn  26210  wwlkextbij  26261  clwwlk  26294  clwwlkn  26295  2wlkonot  26392  2spthonot  26393  2wlksot  26394  2spthsot  26395  vdgrf  26425  vdgrun  26428  vdusgraval  26434  hashnbgravdg  26440  usgravd0nedg  26445  rusgranumwwlkl1  26473  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrawopreglem1  26571  usg2spot2nb  26592  usgreg2spot  26594  2spotmdisj  26595  usgreghash2spot  26596  rabfodom  28728  ordtrest2NEWlem  29296  hasheuni  29474  sigaval  29500  ldgenpisyslem1  29553  ddemeas  29626  braew  29632  imambfm  29651  carsgval  29692  iscvm  30495  cvmsval  30502  fwddifval  31439  fnessref  31522  indexa  32698  supex2g  32702  rfovfvfvd  37317  rfovcnvf1od  37318  fsovfvfvd  37325  fsovcnvlem  37327  cnfex  38210  stoweidlem26  38919  stoweidlem31  38924  stoweidlem34  38927  stoweidlem46  38939  stoweidlem59  38952  salexct  39228  caragenval  39383  fusgredgfi  40544  nbgrval  40560  cusgrsize  40670  wwlks  41038  wwlksnextbij  41108  clwwlks  41187  vdn0conngrumgrv2  41363  vdgn1frgrv2  41466  frgrwopreglem1  41481  dmatALTbas  41984  lcoop  41994