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

Theorem rabex 3960
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 3959 . 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 1436   {crab 2359   _Vcvv 2615
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rab 2364  df-v 2617  df-in 2994  df-ss 3001
This theorem is referenced by:  repizf2  3974  undifexmid  4004  exmidexmid  4007  ordtriexmidlem  4311  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  regexmid  4326  reg2exmid  4327  reg3exmid  4370  nnregexmid  4409  ssimaex  5330  acexmidlemcase  5610  acexmidlemv  5613  fnpm  6367  ssfiexmid  6546  domfiexmid  6548  inffiexmid  6576  genpelvl  7018  genpelvu  7019  genipdm  7022  ltexprlemell  7104  ltexprlemelu  7105  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemlol  7153  cauappcvgprlemopu  7154  cauappcvgprlemupu  7155  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlem2  7166  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemlol  7176  caucvgprlemopu  7177  caucvgprlemupu  7178  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemladdfu  7183  caucvgprlem2  7186  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemexbt  7212  caucvgprprlem2  7216  dfuzi  8792  uzval  8956  ixxval  9249  fzval  9361  oddennn  11111  evenennn  11112  znnen  11117  nninfex  11370
  Copyright terms: Public domain W3C validator