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

Theorem rspcev 2715
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 1464 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspce 2710 1 ((𝐴𝐵𝜓) → ∃𝑥𝐵 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1287  wcel 1436  wrex 2356
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617
This theorem is referenced by:  rspc2ev  2728  rspc3ev  2730  reu6i  2797  rspesbca  2912  nn0suc  4392  elrnmpt1s  4653  elrnrexdm  5401  eldmrexrn  5403  foco2  5494  elabrex  5498  f1elima  5513  fcofo  5524  fliftfun  5536  fliftval  5540  f1oiso2  5567  fo1st  5885  fo2nd  5886  tfr0dm  6041  tfrlemisucaccv  6044  tfrlemi14d  6052  tfrexlem  6053  tfr1onlemsucaccv  6060  tfr1onlemres  6068  tfrcllemsucaccv  6073  tfrcllemres  6081  rdgss  6102  frecabcl  6118  nnaordex  6238  nnawordex  6239  ecelqsg  6297  snfig  6483  nnfi  6540  findcard  6556  fimax2gtrilemstep  6568  unsnfi  6581  eqsupti  6635  supmaxti  6643  supisoex  6648  infminti  6666  djur  6701  finomni  6740  fodjuomnilem0  6746  isnumi  6754  oncardval  6758  archnqq  6920  prarloclemarch2  6922  prcdnql  6987  prcunqu  6988  prarloclemlo  6997  prarloclem5  7003  nqprm  7045  1idprl  7093  1idpru  7094  ltexpri  7116  prplnqu  7123  recexprlemm  7127  recexprlem1ssl  7136  recexprlem1ssu  7137  recexpr  7141  aptiprleml  7142  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemloc  7155  cauappcvgprlem1  7162  cauappcvgprlem2  7163  cauappcvgpr  7165  caucvgprlemm  7171  caucvgprlemloc  7178  caucvgprlem1  7182  caucvgprlem2  7183  caucvgpr  7185  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlem1  7212  caucvgprprlem2  7213  caucvgprpr  7215  negexsr  7262  recexgt0sr  7263  caucvgsrlemgt1  7284  caucvgsrlemoffres  7289  axrnegex  7358  axprecex  7359  nntopi  7373  axcaucvglemres  7378  cnegex  7604  recexre  7996  recexap  8061  receuap  8077  cju  8356  nn2ge  8389  nominpos  8586  zdiv  8767  btwnz  8798  supinfneg  9015  infsupneg  9016  ublbneg  9030  lbzbi  9033  zq  9043  z2ge  9220  iccsupr  9316  exbtwnzlemstep  9587  exbtwnzlemex  9589  rebtwn2zlemstep  9592  rebtwn2z  9594  qbtwnre  9596  qbtwnxr  9597  expnbnd  9974  hashunlem  10109  shftlem  10147  shftfvalg  10149  shftfval  10152  caucvgre  10310  cvg1nlemres  10314  rexanuz  10317  rexuz3  10319  resqrexlemex  10354  caubnd2  10446  maxabslemval  10537  maxleast  10542  rexanre  10549  rexico  10550  fimaxre2  10553  minmax  10556  climconst  10573  climshftlemg  10585  cn1lem  10596  serif0  10633  zisum  10665  fisum  10667  fisumcvg3  10676  dvdsval2  10681  dvds0lem  10688  dvds1lem  10689  dvds2lem  10690  odd2np1lem  10754  odd2np1  10755  opeo  10779  omeo  10780  divalglemex  10804  zsupcllemstep  10823  infssuzex  10827  bezoutlemnewy  10867  bezoutlemaz  10874  bezoutlembz  10875  bezoutlemsup  10880  ncoprmgcdne1b  10953  exprmfct  11001  bj-nn0suc0  11290  bj-inf2vnlem1  11310  nninfsellemeq  11351  nninfomnilem  11355  qdencn  11360
  Copyright terms: Public domain W3C validator