Theorem rabexg 5006

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

Syntax hints:   → wi 4   ∈ wcel 2157  {crab 3093  Vcvv 3385   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-in 3776  df-ss 3783

This theorem is referenced by:  rabex  5007  rabexd  5008  class2set  5024  exse  5276  elfvmptrab1  6530  elovmpt2rab  7114  elovmpt2rab1  7115  ovmpt3rabdm  7126  elovmpt3rab1  7127  suppval  7534  mpt2xopoveq  7583  wdom2d  8727  scottex  8998  tskwe  9062  fin1a2lem12  9521  hashbclem  13485  wrdnfi  13568  wrd2f1tovbij  14046  hashdvds  15813  hashbcval  16039  brric  19062  psrass1lem  19700  psrcom  19732  dmatval  20624  cpmat  20842  fctop  21137  cctop  21139  ppttop  21140  epttop  21142  cldval  21156  neif  21233  neival  21235  neiptoptop  21264  neiptopnei  21265  ordtbaslem  21321  ordtbas2  21324  ordtopn1  21327  ordtopn2  21328  ordtrest2lem  21336  cmpsublem  21531  kgenval  21667  qtopval  21827  kqfval  21855  ordthmeolem  21933  elmptrab  21959  fbssfi  21969  fgval  22002  flimval  22095  flimfnfcls  22160  ptcmplem2  22185  ptcmplem3  22186  tsmsfbas  22259  eltsms  22264  utopval  22364  blvalps  22518  blval  22519  minveclem3b  23538  minveclem3  23539  minveclem4  23542  fusgredgfi  26559  nbgrval  26571  cusgrsize  26704  wwlks  27086  wwlksnextbij  27179  wwlksnextbijOLD  27180  clwwlk  27276  vdn0conngrumgrv2  27540  vdgn1frgrv2  27645  frgrwopreglem1  27661  rabfodom  29862  ordtrest2NEWlem  30484  hasheuni  30663  sigaval  30689  ldgenpisyslem1  30742  ddemeas  30815  braew  30821  imambfm  30840  carsgval  30881  iscvm  31758  cvmsval  31765  fwddifval  32782  fnessref  32864  indexa  34016  supex2g  34020  rfovfvfvd  39079  rfovcnvf1od  39080  fsovfvfvd  39087  fsovcnvlem  39089  cnfex  39947  stoweidlem26  40986  stoweidlem31  40991  stoweidlem34  40994  stoweidlem46  41006  stoweidlem59  41019  salexct  41295  caragenval  41453  dmatALTbas  42989  lcoop  42999