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

Theorem rabex 3930
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 3929 . 2  |-  ( A  e.  _V  ->  { x  e.  A  |  ph }  e.  _V )
31, 2ax-mp 7 1  |-  { x  e.  A  |  ph }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1434   {crab 2353   _Vcvv 2602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rab 2358  df-v 2604  df-in 2980  df-ss 2987
This theorem is referenced by:  repizf2  3944  ordtriexmidlem  4271  ordtri2or2exmidlem  4277  onsucelsucexmidlem  4280  regexmid  4286  reg2exmid  4287  reg3exmid  4330  nnregexmid  4368  ssimaex  5266  acexmidlemcase  5538  acexmidlemv  5541  ssfiexmid  6411  domfiexmid  6413  genpelvl  6764  genpelvu  6765  genipdm  6768  ltexprlemell  6850  ltexprlemelu  6851  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlem2  6912  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlem2  6932  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemexbt  6958  caucvgprprlem2  6962  dfuzi  8538  uzval  8702  ixxval  8995  fzval  9107  oddennn  10703  evenennn  10704  znnen  10709
  Copyright terms: Public domain W3C validator