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

Theorem rabex 4072
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.)
Hypothesis
Ref Expression
rabex.1 𝐴 ∈ V
Assertion
Ref Expression
rabex {𝑥𝐴𝜑} ∈ V
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabex
StepHypRef Expression
1 rabex.1 . 2 𝐴 ∈ V
2 rabexg 4071 . 2 (𝐴 ∈ V → {𝑥𝐴𝜑} ∈ V)
31, 2ax-mp 5 1 {𝑥𝐴𝜑} ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1480  {crab 2420  Vcvv 2686
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rab 2425  df-v 2688  df-in 3077  df-ss 3084
This theorem is referenced by:  repizf2  4086  undifexmid  4117  exmidexmid  4120  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  regexmid  4450  reg2exmid  4451  reg3exmid  4494  nnregexmid  4534  ssimaex  5482  acexmidlemcase  5769  acexmidlemv  5772  fnpm  6550  ssfiexmid  6770  domfiexmid  6772  inffiexmid  6800  ctssdclemr  6997  ctssexmid  7024  exmidonfinlem  7049  exmidaclem  7064  genpelvl  7327  genpelvu  7328  genipdm  7331  ltexprlemell  7413  ltexprlemelu  7414  cauappcvgprlemm  7460  cauappcvgprlemopl  7461  cauappcvgprlemlol  7462  cauappcvgprlemopu  7463  cauappcvgprlemupu  7464  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdfu  7469  cauappcvgprlemladdfl  7470  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  cauappcvgprlem1  7474  cauappcvgprlem2  7475  caucvgprlemm  7483  caucvgprlemopl  7484  caucvgprlemlol  7485  caucvgprlemopu  7486  caucvgprlemupu  7487  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlemladdfu  7492  caucvgprlem2  7495  caucvgprprlemell  7500  caucvgprprlemelu  7501  caucvgprprlemml  7509  caucvgprprlemmu  7510  caucvgprprlemexbt  7521  caucvgprprlem2  7525  suplocexprlem2b  7529  suplocexprlemlub  7539  sup3exmid  8722  dfuzi  9168  uzval  9335  ixxval  9686  fzval  9799  oddennn  11912  evenennn  11913  znnen  11918  ctiunct  11960  fncld  12277  xmetunirn  12537  limccl  12807  ellimc3apf  12808  subctctexmid  13226  nninfex  13235
  Copyright terms: Public domain W3C validator