MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabexg Structured version   Visualization version   GIF version

Theorem rabexg 5233
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
StepHypRef Expression
1 ssrab2 4055 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
2 ssexg 5226 . 2 (({𝑥𝐴𝜑} ⊆ 𝐴𝐴𝑉) → {𝑥𝐴𝜑} ∈ V)
31, 2mpan 688 1 (𝐴𝑉 → {𝑥𝐴𝜑} ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  {crab 3142  Vcvv 3494  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951
This theorem is referenced by:  rabex  5234  rabexd  5235  class2set  5253  exse  5518  elfvmptrab1w  6793  elfvmptrab1  6794  elovmporab  7390  elovmporab1w  7391  elovmporab1  7392  ovmpt3rabdm  7403  elovmpt3rab1  7404  suppval  7831  mpoxopoveq  7884  wdom2d  9043  scottex  9313  tskwe  9378  fin1a2lem12  9832  hashbclem  13809  wrdnfi  13898  wrdnfiOLD  13899  wrd2f1tovbij  14323  hashdvds  16111  hashbcval  16337  brric  19498  psrass1lem  20156  psrcom  20188  dmatval  21100  cpmat  21316  fctop  21611  cctop  21613  ppttop  21614  epttop  21616  cldval  21630  neif  21707  neival  21709  neiptoptop  21738  neiptopnei  21739  ordtbaslem  21795  ordtbas2  21798  ordtopn1  21801  ordtopn2  21802  ordtrest2lem  21810  cmpsublem  22006  kgenval  22142  qtopval  22302  kqfval  22330  ordthmeolem  22408  elmptrab  22434  fbssfi  22444  fgval  22477  flimval  22570  flimfnfcls  22635  ptcmplem2  22660  ptcmplem3  22661  tsmsfbas  22735  eltsms  22740  utopval  22840  blvalps  22994  blval  22995  minveclem3b  24030  minveclem3  24031  minveclem4  24034  fusgredgfi  27106  nbgrval  27117  cusgrsize  27235  wwlks  27612  wwlksnextbij  27679  clwwlk  27760  vdn0conngrumgrv2  27974  vdgn1frgrv2  28074  frgrwopreglem1  28090  rabfodom  30265  ordtrest2NEWlem  31165  hasheuni  31344  sigaval  31370  ldgenpisyslem1  31422  ddemeas  31495  braew  31501  imambfm  31520  carsgval  31561  iscvm  32506  cvmsval  32513  fwddifval  33623  fnessref  33705  indexa  35007  supex2g  35011  rfovfvfvd  40349  rfovcnvf1od  40350  fsovfvfvd  40357  fsovcnvlem  40359  cnfex  41285  stoweidlem26  42312  stoweidlem31  42317  stoweidlem34  42320  stoweidlem46  42332  stoweidlem59  42345  salexct  42618  caragenval  42776  dmatALTbas  44457  lcoop  44467
  Copyright terms: Public domain W3C validator