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

Theorem rspcev 2712
Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcev  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcev
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2707 1  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285    e. wcel 1434   E.wrex 2354
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 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2614
This theorem is referenced by:  rspc2ev  2725  rspc3ev  2727  reu6i  2794  rspesbca  2909  nn0suc  4381  elrnmpt1s  4641  elrnrexdm  5381  eldmrexrn  5383  foco2  5471  elabrex  5475  f1elima  5490  fcofo  5501  fliftfun  5513  fliftval  5517  f1oiso2  5543  fo1st  5861  fo2nd  5862  tfr0dm  6017  tfrlemisucaccv  6020  tfrlemi14d  6028  tfrexlem  6029  tfr1onlemsucaccv  6036  tfr1onlemres  6044  tfrcllemsucaccv  6049  tfrcllemres  6057  rdgss  6078  frecabcl  6094  nnaordex  6214  nnawordex  6215  ecelqsg  6273  snfig  6459  nnfi  6516  findcard  6532  unsnfi  6554  eqsupti  6596  supmaxti  6604  supisoex  6609  infminti  6627  djur  6662  finomni  6699  fodjuomnilem0  6705  isnumi  6711  oncardval  6715  archnqq  6877  prarloclemarch2  6879  prcdnql  6944  prcunqu  6945  prarloclemlo  6954  prarloclem5  6960  nqprm  7002  1idprl  7050  1idpru  7051  ltexpri  7073  prplnqu  7080  recexprlemm  7084  recexprlem1ssl  7093  recexprlem1ssu  7094  recexpr  7098  aptiprleml  7099  archpr  7103  cauappcvgprlemm  7105  cauappcvgprlemloc  7112  cauappcvgprlem1  7119  cauappcvgprlem2  7120  cauappcvgpr  7122  caucvgprlemm  7128  caucvgprlemloc  7135  caucvgprlem1  7139  caucvgprlem2  7140  caucvgpr  7142  caucvgprprlemmu  7155  caucvgprprlemopl  7157  caucvgprprlemopu  7159  caucvgprprlemloc  7163  caucvgprprlem1  7169  caucvgprprlem2  7170  caucvgprpr  7172  negexsr  7219  recexgt0sr  7220  caucvgsrlemgt1  7241  caucvgsrlemoffres  7246  axrnegex  7315  axprecex  7316  nntopi  7330  axcaucvglemres  7335  cnegex  7561  recexre  7953  recexap  8018  receuap  8034  cju  8313  nn2ge  8346  nominpos  8543  zdiv  8728  btwnz  8759  supinfneg  8976  infsupneg  8977  ublbneg  8991  lbzbi  8994  zq  9004  z2ge  9181  iccsupr  9277  exbtwnzlemstep  9546  exbtwnzlemex  9548  rebtwn2zlemstep  9551  rebtwn2z  9553  qbtwnre  9555  qbtwnxr  9556  expnbnd  9910  hashunlem  10045  shftlem  10076  shftfvalg  10078  shftfval  10081  caucvgre  10239  cvg1nlemres  10243  rexanuz  10246  rexuz3  10248  resqrexlemex  10283  caubnd2  10375  maxabslemval  10466  maxleast  10471  rexanre  10478  rexico  10479  fimaxre2  10481  minmax  10484  climconst  10501  climshftlemg  10513  cn1lem  10524  serif0  10561  dvdsval2  10577  dvds0lem  10584  dvds1lem  10585  dvds2lem  10586  odd2np1lem  10650  odd2np1  10651  opeo  10675  omeo  10676  divalglemex  10700  zsupcllemstep  10719  infssuzex  10723  bezoutlemnewy  10763  bezoutlemaz  10770  bezoutlembz  10771  bezoutlemsup  10776  ncoprmgcdne1b  10849  exprmfct  10897  bj-nn0suc0  11186  bj-inf2vnlem1  11206  qdencn  11226
  Copyright terms: Public domain W3C validator