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

Theorem rspcev 2673
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 1437 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2668 1  |-  ( ( A  e.  B  /\  ps )  ->  E. x  e.  B  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102    = wceq 1259    e. wcel 1409   E.wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576
This theorem is referenced by:  rspc2ev  2686  rspc3ev  2688  reu6i  2754  rspesbca  2869  nn0suc  4354  elrnmpt1s  4611  elrnrexdm  5333  eldmrexrn  5335  foco2  5345  elabrex  5424  f1elima  5439  fcofo  5451  fliftfun  5463  fliftval  5467  f1oiso2  5493  fo1st  5811  fo2nd  5812  tfr0  5967  tfrlemisucaccv  5969  tfrlemi14d  5977  tfrexlem  5978  rdgss  6000  nnaordex  6130  nnawordex  6131  ecelqsg  6189  snfig  6321  nnfi  6363  findcard  6375  eqsupti  6401  supmaxti  6407  supisoex  6412  isnumi  6419  oncardval  6423  archnqq  6572  prarloclemarch2  6574  prcdnql  6639  prcunqu  6640  prarloclemlo  6649  prarloclem5  6655  nqprm  6697  1idprl  6745  1idpru  6746  ltexpri  6768  prplnqu  6775  recexprlemm  6779  recexprlem1ssl  6788  recexprlem1ssu  6789  recexpr  6793  aptiprleml  6794  archpr  6798  cauappcvgprlemm  6800  cauappcvgprlemloc  6807  cauappcvgprlem1  6814  cauappcvgprlem2  6815  cauappcvgpr  6817  caucvgprlemm  6823  caucvgprlemloc  6830  caucvgprlem1  6834  caucvgprlem2  6835  caucvgpr  6837  caucvgprprlemmu  6850  caucvgprprlemopl  6852  caucvgprprlemopu  6854  caucvgprprlemloc  6858  caucvgprprlem1  6864  caucvgprprlem2  6865  caucvgprpr  6867  negexsr  6914  recexgt0sr  6915  caucvgsrlemgt1  6936  caucvgsrlemoffres  6941  axrnegex  7010  axprecex  7011  nntopi  7025  axcaucvglemres  7030  cnegex  7251  recexre  7642  recexap  7707  receuap  7723  cju  7988  nn2ge  8021  nominpos  8218  zdiv  8385  btwnz  8415  ublbneg  8644  lbzbi  8647  zq  8657  z2ge  8839  iccsupr  8935  qbtwnzlemstep  9204  qbtwnzlemex  9206  rebtwn2zlemstep  9208  rebtwn2z  9210  qbtwnre  9212  qbtwnxr  9213  expnbnd  9539  shftlem  9644  shftfvalg  9646  shftfval  9649  caucvgre  9807  cvg1nlemres  9811  rexanuz  9814  rexuz3  9816  resqrexlemex  9851  caubnd2  9943  climconst  10041  climshftlemg  10053  cn1lem  10064  serif0  10101  dvdsval2  10110  dvds0lem  10117  dvds1lem  10118  dvds2lem  10119  odd2np1lem  10182  odd2np1  10183  opeo  10208  omeo  10209  bj-nn0suc0  10441  bj-inf2vnlem1  10461  qdencn  10490
  Copyright terms: Public domain W3C validator