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

Theorem rspcev 2702
Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcev ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev
StepHypRef Expression
1 nfv 1462 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspce 2697 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wcel 1434  wrex 2350
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 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604
This theorem is referenced by:  rspc2ev  2716  rspc3ev  2718  reu6i  2784  rspesbca  2899  nn0suc  4353  elrnmpt1s  4612  elrnrexdm  5338  eldmrexrn  5340  foco2  5350  elabrex  5429  f1elima  5444  fcofo  5455  fliftfun  5467  fliftval  5471  f1oiso2  5497  fo1st  5815  fo2nd  5816  tfr0dm  5971  tfrlemisucaccv  5974  tfrlemi14d  5982  tfrexlem  5983  tfr1onlemsucaccv  5990  tfr1onlemres  5998  tfrcllemsucaccv  6003  tfrcllemres  6011  rdgss  6032  frecabcl  6048  nnaordex  6166  nnawordex  6167  ecelqsg  6225  snfig  6359  nnfi  6407  findcard  6422  unsnfi  6439  eqsupti  6468  supmaxti  6476  supisoex  6481  infminti  6499  isnumi  6510  oncardval  6514  archnqq  6669  prarloclemarch2  6671  prcdnql  6736  prcunqu  6737  prarloclemlo  6746  prarloclem5  6752  nqprm  6794  1idprl  6842  1idpru  6843  ltexpri  6865  prplnqu  6872  recexprlemm  6876  recexprlem1ssl  6885  recexprlem1ssu  6886  recexpr  6890  aptiprleml  6891  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemloc  6904  cauappcvgprlem1  6911  cauappcvgprlem2  6912  cauappcvgpr  6914  caucvgprlemm  6920  caucvgprlemloc  6927  caucvgprlem1  6931  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgprpr  6964  negexsr  7011  recexgt0sr  7012  caucvgsrlemgt1  7033  caucvgsrlemoffres  7038  axrnegex  7107  axprecex  7108  nntopi  7122  axcaucvglemres  7127  cnegex  7353  recexre  7745  recexap  7810  receuap  7826  cju  8105  nn2ge  8138  nominpos  8335  zdiv  8516  btwnz  8547  supinfneg  8764  infsupneg  8765  ublbneg  8779  lbzbi  8782  zq  8792  z2ge  8969  iccsupr  9065  exbtwnzlemstep  9334  exbtwnzlemex  9336  rebtwn2zlemstep  9339  rebtwn2z  9341  qbtwnre  9343  qbtwnxr  9344  expnbnd  9693  sizeunlem  9828  shftlem  9842  shftfvalg  9844  shftfval  9847  caucvgre  10005  cvg1nlemres  10009  rexanuz  10012  rexuz3  10014  resqrexlemex  10049  caubnd2  10141  maxabslemval  10232  maxleast  10237  rexanre  10244  rexico  10245  fimaxre2  10247  minmax  10250  climconst  10267  climshftlemg  10279  cn1lem  10290  serif0  10327  dvdsval2  10343  dvds0lem  10350  dvds1lem  10351  dvds2lem  10352  odd2np1lem  10416  odd2np1  10417  opeo  10441  omeo  10442  divalglemex  10466  zsupcllemstep  10485  infssuzex  10489  bezoutlemnewy  10529  bezoutlemaz  10536  bezoutlembz  10537  bezoutlemsup  10542  ncoprmgcdne1b  10615  exprmfct  10663  bj-nn0suc0  10903  bj-inf2vnlem1  10923  qdencn  10943
  Copyright terms: Public domain W3C validator