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

Theorem rspcev 2722
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 1466 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspce 2717 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 1289    e. wcel 1438   E.wrex 2360
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-v 2621
This theorem is referenced by:  rspc2ev  2735  rspc3ev  2737  reu6i  2804  rspesbca  2921  nn0suc  4409  elrnmpt1s  4673  elrnrexdm  5422  eldmrexrn  5424  foco2  5515  elabrex  5519  f1elima  5534  fcofo  5545  fliftfun  5557  fliftval  5561  f1oiso2  5588  fo1st  5910  fo2nd  5911  tfr0dm  6069  tfrlemisucaccv  6072  tfrlemi14d  6080  tfrexlem  6081  tfr1onlemsucaccv  6088  tfr1onlemres  6096  tfrcllemsucaccv  6101  tfrcllemres  6109  rdgss  6130  frecabcl  6146  nnaordex  6266  nnawordex  6267  ecelqsg  6325  snfig  6511  nnfi  6568  findcard  6584  fimax2gtrilemstep  6596  unsnfi  6609  eqsupti  6670  supmaxti  6678  supisoex  6683  infminti  6701  djur  6736  finomni  6775  fodjuomnilem0  6781  isnumi  6789  oncardval  6793  archnqq  6955  prarloclemarch2  6957  prcdnql  7022  prcunqu  7023  prarloclemlo  7032  prarloclem5  7038  nqprm  7080  1idprl  7128  1idpru  7129  ltexpri  7151  prplnqu  7158  recexprlemm  7162  recexprlem1ssl  7171  recexprlem1ssu  7172  recexpr  7176  aptiprleml  7177  archpr  7181  cauappcvgprlemm  7183  cauappcvgprlemloc  7190  cauappcvgprlem1  7197  cauappcvgprlem2  7198  cauappcvgpr  7200  caucvgprlemm  7206  caucvgprlemloc  7213  caucvgprlem1  7217  caucvgprlem2  7218  caucvgpr  7220  caucvgprprlemmu  7233  caucvgprprlemopl  7235  caucvgprprlemopu  7237  caucvgprprlemloc  7241  caucvgprprlem1  7247  caucvgprprlem2  7248  caucvgprpr  7250  negexsr  7297  recexgt0sr  7298  caucvgsrlemgt1  7319  caucvgsrlemoffres  7324  axrnegex  7393  axprecex  7394  nntopi  7408  axcaucvglemres  7413  cnegex  7639  recexre  8031  recexap  8096  receuap  8112  cju  8393  nn2ge  8426  nominpos  8623  zdiv  8804  btwnz  8835  supinfneg  9052  infsupneg  9053  ublbneg  9067  lbzbi  9070  zq  9080  z2ge  9257  iccsupr  9353  exbtwnzlemstep  9624  exbtwnzlemex  9626  rebtwn2zlemstep  9629  rebtwn2z  9631  qbtwnre  9633  qbtwnxr  9634  expnbnd  10042  hashunlem  10177  shftlem  10215  shftfvalg  10217  shftfval  10220  caucvgre  10379  cvg1nlemres  10383  rexanuz  10386  rexuz3  10388  resqrexlemex  10423  caubnd2  10515  maxabslemval  10606  maxleast  10611  rexanre  10618  rexico  10619  fimaxre2  10622  minmax  10625  climconst  10642  climshftlemg  10654  cn1lem  10666  serif0  10705  zisum  10738  fisum  10742  fisumcvg3  10752  dvdsval2  10892  dvds0lem  10899  dvds1lem  10900  dvds2lem  10901  odd2np1lem  10965  odd2np1  10966  opeo  10990  omeo  10991  divalglemex  11015  zsupcllemstep  11034  infssuzex  11038  bezoutlemnewy  11078  bezoutlemaz  11085  bezoutlembz  11086  bezoutlemsup  11091  ncoprmgcdne1b  11164  exprmfct  11212  bj-nn0suc0  11502  bj-inf2vnlem1  11522  nninfsellemeq  11563  nninfomnilem  11567  qdencn  11572
  Copyright terms: Public domain W3C validator