ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rabex Unicode version

Theorem rabex 4079
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
rabex.1  |-  A  e. 
_V
Assertion
Ref Expression
rabex  |-  { x  e.  A  |  ph }  e.  _V
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rabex
StepHypRef Expression
1 rabex.1 . 2  |-  A  e. 
_V
2 rabexg 4078 . 2  |-  ( A  e.  _V  ->  { x  e.  A  |  ph }  e.  _V )
31, 2ax-mp 5 1  |-  { x  e.  A  |  ph }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1481   {crab 2421   _Vcvv 2689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-v 2691  df-in 3081  df-ss 3088
This theorem is referenced by:  repizf2  4093  undifexmid  4124  exmidexmid  4127  ordtriexmidlem  4442  ordtri2or2exmidlem  4448  onsucelsucexmidlem  4451  regexmid  4457  reg2exmid  4458  reg3exmid  4501  nnregexmid  4541  ssimaex  5489  acexmidlemcase  5776  acexmidlemv  5779  fnpm  6557  ssfiexmid  6777  domfiexmid  6779  inffiexmid  6807  ctssdclemr  7004  ctssexmid  7031  exmidonfinlem  7065  exmidaclem  7080  genpelvl  7343  genpelvu  7344  genipdm  7347  ltexprlemell  7429  ltexprlemelu  7430  cauappcvgprlemm  7476  cauappcvgprlemopl  7477  cauappcvgprlemlol  7478  cauappcvgprlemopu  7479  cauappcvgprlemupu  7480  cauappcvgprlemdisj  7482  cauappcvgprlemloc  7483  cauappcvgprlemladdfu  7485  cauappcvgprlemladdfl  7486  cauappcvgprlemladdru  7487  cauappcvgprlemladdrl  7488  cauappcvgprlem1  7490  cauappcvgprlem2  7491  caucvgprlemm  7499  caucvgprlemopl  7500  caucvgprlemlol  7501  caucvgprlemopu  7502  caucvgprlemupu  7503  caucvgprlemdisj  7505  caucvgprlemloc  7506  caucvgprlemladdfu  7508  caucvgprlem2  7511  caucvgprprlemell  7516  caucvgprprlemelu  7517  caucvgprprlemml  7525  caucvgprprlemmu  7526  caucvgprprlemexbt  7537  caucvgprprlem2  7541  suplocexprlem2b  7545  suplocexprlemlub  7555  sup3exmid  8738  dfuzi  9184  uzval  9351  ixxval  9708  fzval  9822  oddennn  11939  evenennn  11940  znnen  11945  ctiunct  11987  fncld  12304  xmetunirn  12564  limccl  12834  ellimc3apf  12835  subctctexmid  13367  nninfex  13378
  Copyright terms: Public domain W3C validator