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

Theorem rabexg 4731
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 3646 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
2 ssexg 4724 . 2 (({𝑥𝐴𝜑} ⊆ 𝐴𝐴𝑉) → {𝑥𝐴𝜑} ∈ V)
31, 2mpan 701 1 (𝐴𝑉 → {𝑥𝐴𝜑} ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  {crab 2896  Vcvv 3169  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-in 3543  df-ss 3550
This theorem is referenced by:  rabex  4732  rabexd  4733  class2set  4750  exse  4989  elfvmptrab1  6195  elovmpt2rab  6752  elovmpt2rab1  6753  ovmpt3rabdm  6764  elovmpt3rab1  6765  suppval  7158  mpt2xopoveq  7206  wdom2d  8342  scottex  8605  tskwe  8633  fin1a2lem12  9090  hashbclem  13042  wrdnfi  13136  wrd2f1tovbij  13494  hashdvds  15261  hashbcval  15487  brric  18510  psrass1lem  19141  psrcom  19173  dmatval  20056  cpmat  20272  fctop  20557  cctop  20559  ppttop  20560  epttop  20562  cldval  20576  neif  20653  neival  20655  neiptoptop  20684  neiptopnei  20685  ordtbaslem  20741  ordtbas2  20744  ordtopn1  20747  ordtopn2  20748  ordtrest2lem  20756  cmpsublem  20951  kgenval  21087  qtopval  21247  kqfval  21275  ordthmeolem  21353  elmptrab  21379  fbssfi  21390  fgval  21423  flimval  21516  flimfnfcls  21581  ptcmplem2  21606  ptcmplem3  21607  tsmsfbas  21680  eltsms  21685  utopval  21785  blvalps  21938  blval  21939  minveclem3b  22921  minveclem3  22922  minveclem4  22925  fiusgraedgfi  25699  nbgraop  25715  isuvtx  25779  wwlk  25972  wwlkn  25973  wwlkextbij  26024  clwwlk  26057  clwwlkn  26058  2wlkonot  26155  2spthonot  26156  2wlksot  26157  2spthsot  26158  vdgrf  26188  vdgrun  26191  vdusgraval  26197  hashnbgravdg  26203  usgravd0nedg  26208  rusgranumwwlkl1  26236  vdn0frgrav2  26313  vdgn0frgrav2  26314  vdn1frgrav2  26315  vdgn1frgrav2  26316  frgrawopreglem1  26334  usg2spot2nb  26355  usgreg2spot  26357  2spotmdisj  26358  usgreghash2spot  26359  rabfodom  28531  ordtrest2NEWlem  29099  hasheuni  29277  sigaval  29303  ldgenpisyslem1  29356  ddemeas  29429  braew  29435  imambfm  29454  carsgval  29495  iscvm  30298  cvmsval  30305  fwddifval  31242  fnessref  31325  indexa  32498  supex2g  32502  rfovfvfvd  37117  rfovcnvf1od  37118  fsovfvfvd  37125  fsovcnvlem  37127  cnfex  38010  stoweidlem26  38720  stoweidlem31  38725  stoweidlem34  38728  stoweidlem46  38740  stoweidlem59  38753  salexct  39029  caragenval  39184  fusgredgfi  40543  nbgrval  40559  cusgrsize  40669  wwlks  41037  wwlksnextbij  41107  clwwlks  41186  vdn0conngrumgrv2  41362  vdgn1frgrv2  41465  frgrwopreglem1  41480  dmatALTbas  41983  lcoop  41993
  Copyright terms: Public domain W3C validator