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

Theorem rabexg 4810
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 3685 . 2 {𝑥𝐴𝜑} ⊆ 𝐴
2 ssexg 4802 . 2 (({𝑥𝐴𝜑} ⊆ 𝐴𝐴𝑉) → {𝑥𝐴𝜑} ∈ V)
31, 2mpan 706 1 (𝐴𝑉 → {𝑥𝐴𝜑} ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  {crab 2915  Vcvv 3198  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rab 2920  df-v 3200  df-in 3579  df-ss 3586
This theorem is referenced by:  rabex  4811  rabexd  4812  class2set  4830  exse  5076  elfvmptrab1  6303  elovmpt2rab  6877  elovmpt2rab1  6878  ovmpt3rabdm  6889  elovmpt3rab1  6890  suppval  7294  mpt2xopoveq  7342  wdom2d  8482  scottex  8745  tskwe  8773  fin1a2lem12  9230  hashbclem  13231  wrdnfi  13333  wrd2f1tovbij  13697  hashdvds  15474  hashbcval  15700  brric  18738  psrass1lem  19371  psrcom  19403  dmatval  20292  cpmat  20508  fctop  20802  cctop  20804  ppttop  20805  epttop  20807  cldval  20821  neif  20898  neival  20900  neiptoptop  20929  neiptopnei  20930  ordtbaslem  20986  ordtbas2  20989  ordtopn1  20992  ordtopn2  20993  ordtrest2lem  21001  cmpsublem  21196  kgenval  21332  qtopval  21492  kqfval  21520  ordthmeolem  21598  elmptrab  21624  fbssfi  21635  fgval  21668  flimval  21761  flimfnfcls  21826  ptcmplem2  21851  ptcmplem3  21852  tsmsfbas  21925  eltsms  21930  utopval  22030  blvalps  22184  blval  22185  minveclem3b  23193  minveclem3  23194  minveclem4  23197  fusgredgfi  26211  nbgrval  26228  cusgrsize  26344  wwlks  26721  wwlksnextbij  26791  clwwlks  26873  vdn0conngrumgrv2  27049  vdgn1frgrv2  27153  frgrwopreglem1  27167  rabfodom  29328  ordtrest2NEWlem  29953  hasheuni  30132  sigaval  30158  ldgenpisyslem1  30211  ddemeas  30284  braew  30290  imambfm  30309  carsgval  30350  iscvm  31226  cvmsval  31233  fwddifval  32253  fnessref  32336  indexa  33508  supex2g  33512  rfovfvfvd  38123  rfovcnvf1od  38124  fsovfvfvd  38131  fsovcnvlem  38133  cnfex  39013  stoweidlem26  40012  stoweidlem31  40017  stoweidlem34  40020  stoweidlem46  40032  stoweidlem59  40045  salexct  40321  caragenval  40476  dmatALTbas  41961  lcoop  41971
  Copyright terms: Public domain W3C validator